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
(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
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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and