Re: [isabelle] soundness of Isabelle/HOL



On 30.01.2012 10:59, Matthias Schmalz wrote:
I already know that Isabelle follows the LCF approach and that HOL is
built from a modest number of axioms using conservative extension
methods. It is therefore very likely that proofs by Isabelle are
correct. I also know that this soundness guarantee is restricted to the
inference core; for example, nothing prevents users from configuring the
parser to parse "False" as "True" and therefore giving the impression
that "False" can be proved. (And of course, soundness rests on the
assumption that compiler, ML libraries, operating system, and hardware
behave correctly.)

I think HOL Zero tries to make sure that you cannot reconfigure parser and pretty-printer in a way that confuses the user. If you search for mark at proof-technologies.com on this list, you should find some discussion on this topic.

  -- Lars





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