Re: [isabelle] Easy And Language Integrated Use



On Sun, 5 Jan 2014, Suminda Dharmasena wrote:

Is it possible to provide a way to use this within Scala IDE and also integrate where you can have verification within the Scala language itself.

(I am answering in isabelle-users *exclusively* since the question is off-topic for isabelle-dev, and cross-posting on both lists is never done. See also http://isabelle.in.tum.de/ for the explanations of the two mailing lists.)


Do you have any particular Scala IDE in mind?

The general problem of having a nice IDE for some programming language plus integrated specification and verification is addressed by various research projects, but this is still far from being ready for prime time. If you look around in the vicinity of the ETAPS / F-IDE workshop http://www.ensta-paristech.fr/~etaps/ you might get some ideas of ongoing work.

Some arbitrary example projects:

  http://www.key-project.org

  http://itu.dk/research/tomeso/kopitiam

  http://research.microsoft.com/en-us/projects/specsharp
  http://research.microsoft.com/en-us/projects/dafny


There are still many accidental and fundamental problems to make it work for mainstream use. In particular, after decades of cumulative programming language design, the results are so complex to make specification and verification very difficult. In fact, Scala is a major player in that feature-bloat category of programming languages.

The SPARK Ada approach is the opposite: some recovery of language sanity, which facilitates serious verification. There are also verification and specification tools for that, to be searched on the web. Isabelle/HOL-SPARK may serve as arbitrary starting to inform yourself further.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.