Re: [isabelle] [isabelle-dev] Circular reasoning via multithreading seems too easy
On 12/12/16 00:19, Randy Pollack wrote:
> 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?
I keep asking that same question whenever I meet people who have to
potential to do it, e.g. the CakeML guys.
Ultimately I would like to see:
(1) A common understanding of HOL as a logic, by all providers of some
(2) An independent programming language implementation (other than
Poly/ML). E.g. verified CakeML or something totally different (verified
Rust?); better not C++ or OCaml.
(3) An independently implemented and maintained HOL proof checker
based on (1) and (2).
As a start, one could target at a proper Isabelle/HOL ~> OpenTheory
export tool. (It will also require some reforms in Isabelle to make it
This archive was generated by a fusion of
Pipermail (Mailman edition) and