*To*: Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr>*Subject*: Re: [isabelle] Isabelle's jEdit plugin: some known help documents?*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Wed, 1 Aug 2012 19:49:47 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <op.wic9pxp6ule2fv@douda-yannick>*References*: <op.wibg4tbsule2fv@douda-yannick> <alpine.LNX.2.00.1207312207020.28712@macbroy21.informatik.tu-muenchen.de> <5018AE62.6020402@gmx.com> <50193054.2050605@gmx.com> <op.wic9pxp6ule2fv@douda-yannick>

Standards are possible when you have a universally agreed upon formalism, such as first-order logic: we have TPTP format. And there is a common format for SMT problems. But even with higher-order logic, there are a great many significant differences concerning the nature of types, for example. When you get to systems such as Isabelle and Coq, you have formalisms that are intrinsically different with almost no common ground between them. Larry Paulson On 1 Aug 2012, at 15:40, Yannick Duchêne (Hibou57) wrote: > Le Wed, 01 Aug 2012 15:34:12 +0200, Gottfried Barrow <gottfried.barrow at gmx.com> a écrit: > >> at this point any success by any proof assistant is beneficial to every other proof assistant. > > Standards always help there. Would be nice if they could be some standard to help interoperability between different proof edition and/or proof checker systems. > > I can see two useful standard kinds. > > The first one, for humane readable proof. Isabelle do this with Isar (which I am still learning), I just know Coq a little bit, but I feel to remember it has similar thing. Some coordination could be an option and leads to a standard there? Isabelle's Isar is generic, I don't know if Coq's equivalent is too. > > The second one, for proof check and validation, not necessarily human readable. This could be comparable to byte-code interpreted language, but for proof. This would not necessarily byte-code based, but low level enough, so that any conforming system could check, validate and trust it (and import/use it!). > > After that two standards, multiple systems could be designed in a conforming way, either as automated prover, semi‑automated, or not automated at‑all, with different kind of UI, user experience and so on, without any fears to see this diversity turning into a kind of jungle. > > There are so many systems among the few dominating ones which are Coq, Isabelle (and something named VDM? still in the place?) and Z environments. A common standard for interoperability would be nice. > > > Markus says: > > “In particular one needs to avoid childish attitudes of "my proof assistant is better than your's".” > > Yes, I understand that point, but for the reasons mentioned above, dealing with standards, I feel Isabelle may be more an option, because it is based on SML (standard, formally specified and verified and with multiple implementation, all unlike OCaml) and may be more standard‑ready with it's rather generic Isar language. > > That said, I don't mean Coq is not nice, I just give the reason why I personally prefer to spend time learning Isabelle instead of Coq (I already had a quick look at Coq and CoqIDE). > > > -- > “Syntactic sugar causes cancer of the semi-colons.” [1] > “Structured Programming supports the law of the excluded muddle.” [1] > [1]: Epigrams on Programming — Alan J. — P. Yale University > >

**References**:**Re: [isabelle] Isabelle's jEdit plugin: some known help documents?***From:*Gottfried Barrow

**Re: [isabelle] Isabelle's jEdit plugin: some known help documents?***From:*Gottfried Barrow

**Re: [isabelle] Isabelle's jEdit plugin: some known help documents?***From:*Yannick Duchêne (Hibou57)

- Previous by Date: [isabelle] termination: Low-Level Exception, Last Function Definition
- Next by Date: [isabelle] Syntax issue: lost between HOL and Isar
- Previous by Thread: Re: [isabelle] Isabelle's jEdit plugin: some known help documents?
- Next by Thread: Re: [isabelle] Some Remarks to Code Generation
- Cl-isabelle-users August 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list