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.
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
Description: S/MIME Cryptographic Signature