[isabelle] soundness of Isabelle/HOL



Hi,

Out of curiosity and for my thesis introduction, I have the following question. I am wondering whether there is a theorem prover out there that gives stronger soundness guarantees than Isabelle/HOL and whether there is empirical evidence showing that the difference is practically relevant. I would also like to know when the last unsoundness bug in Isabelle's inference core has been observed.

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

Many thanks in advance,
Matthias





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