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
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.
“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.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and