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



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?

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
>
>
>




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