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 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 you might get some ideas of ongoing work.

Some arbitrary example projects:

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.


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