Re: [isabelle] soundness of Isabelle/HOL



Forgive me if I launch into my usual lecture: I have never seen a piece of work spoilt by soundness bugs in a theorem prover. I have seen many pieces of work spoilt by unrealistic models, incorrect axioms or proofs of irrelevant properties. Soundness is vital, but (contrary to a widely held belief) it doesn't absolve users of the need to know what they are doing.

Larry Paulson


On 30 Jan 2012, at 09:59, Matthias Schmalz wrote:

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