Email Gateway (Aug 19 2022 at 13:26): Email Gateway (Aug 19 2022 at 13:26):From: Suminda Dharmasena <sirinath@sakrio.com>
Hi,
Many thanks for the response. Scala IDE (http://scala-ide.org/)
There is https://github.com/epfl-lara/leon but this does not ready fro
prime time.
Suminda
--
Suminda Sirinath Salpitikorala Dharmasena, B.Sc. Comp. & I.S. (Hon.) Lond.,
P.G.Dip. Ind. Maths. J'Pura, MIEEE, MACM, CEO Sakrīō! ▣ Address: 6G • 1st
Lane • Pagoda Road • Nugegoda 10250 • Sri Lanka. ▣ Mobile
: +94-(0)711007945 ▣ Office: +94-(0) 11 2 199766 ▣ Home Office: +94-(0)
11-5 875614 ▣ Home: +94-(0)11-5 864614 / 2 825908 ▣ Web:
http://www.sakrio.com ▣
This email is subjected to the email Terms of Use and Disclaimer:
http://www.sakrio.com/email-legal. Please read this first.
--
Email Gateway (Aug 19 2022 at 13:32):From: Suminda Dharmasena <sirinath@sakrio.com>
Hi,
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.
Suminda
Email Gateway (Aug 19 2022 at 13:33):From: Makarius <makarius@sketis.net>
(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://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
Last updated: Apr 27 2024 at 04:17 UTC