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
HOL variant.

  (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
really fit.)


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