Re: [isabelle] Easy And Language Integrated Use



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.
--


On 6 January 2014 19:13, Makarius <makarius at sketis.net> wrote:

>  [image: Boxbe] <https://www.boxbe.com/overview> Makarius (
> makarius at sketis.net) is not on your Guest List<https://www.boxbe.com/approved-list?tc_serial=16044524704&tc_rand=1773410152&utm_source=stf&utm_medium=email&utm_campaign=ANNO_MWTP&utm_content=001&token=Z8b5P99BaCviu769GL%2B%2F35Ql2RVtt%2BDg02lPL%2FLcRF9%2BshUkoQlI8gysFP7FzAe2&key=%2Bpt%2F579zqYZHI4EJMjdO0rYlNRp6rHKt7tApGj%2BcYiE%3D>| Approve
> sender<https://www.boxbe.com/anno?tc_serial=16044524704&tc_rand=1773410152&utm_source=stf&utm_medium=email&utm_campaign=ANNO_MWTP&utm_content=001&token=Z8b5P99BaCviu769GL%2B%2F35Ql2RVtt%2BDg02lPL%2FLcRF9%2BshUkoQlI8gysFP7FzAe2&key=%2Bpt%2F579zqYZHI4EJMjdO0rYlNRp6rHKt7tApGj%2BcYiE%3D>| Approve
> domain<https://www.boxbe.com/anno?tc_serial=16044524704&tc_rand=1773410152&utm_source=stf&utm_medium=email&utm_campaign=ANNO_MWTP&utm_content=001&dom&token=Z8b5P99BaCviu769GL%2B%2F35Ql2RVtt%2BDg02lPL%2FLcRF9%2BshUkoQlI8gysFP7FzAe2&key=%2Bpt%2F579zqYZHI4EJMjdO0rYlNRp6rHKt7tApGj%2BcYiE%3D>
>
> 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.