Re: [isabelle] [isabelle-dev] Circular reasoning via multithreading seems too easy




On 12/12/2016 00:19, Randy Pollack wrote:
Absolute certainty cannot be obtained by millions of lines of code
(prover, compiler, OS, ...) running on real hardware, but, as Hugo
points out, independent checking goes some ways toward improved
confidence.

Truly independent checking is asking a lot of a reader of a formal
development, but Coq has stand-alone
coqchk; some HOLs can be checked by HOL-zero.

What is the story for stand-alone checking of Isabelle/Hol developments?

There are proof terms in Isabelle/HOL, but they share a lot of the infrastructure with the rest of the system. In this example, however, they do the right thing: calling Proof_Checker.thm_of_proof with the proof term for the circular proof fails.

Tobias

On Sun, Dec 11, 2016 at 10:48 PM, Makarius <makarius at sketis.net> wrote:
On 11/12/16 23:17, Makarius wrote:

We need more clarity and more honesty.

Hugo Herbelin is actually an expert an that.

Here is an example from a recent thread on coq-club "safe interface for
writing Coq plugins"
https://sympa.inria.fr/sympa/arc/coq-club/2016-11/msg00080.html (a
"plugin" is just an OCaml module produced by the user; in Isabelle/ML
that is trivial and does not need a special name).

That is an accurate and calm explanation of the realities of Coq,
without causing an uproar on the mailing list. Very professional.


        Makarius





Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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