Re: [isabelle] Isabelle's jEdit plugin: some known help documents?



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






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