Re: [isabelle] soundness of Isabelle/HOL

Larry, you rightly point out that there are more important worries for
theorem prover users.  But this doesn't mean that soundness-related
vulnerabilities should be ignored now.

And also, importantly, I would say that theorem proving hasn't yet reached
its potential.  Nowadays formal proof is largely confined to university
departments and a handful of reputed specialist companies.  If/when theorem
proving does become big, commercial realities mean that there will be
considerable outsourcing of proofs to contractors.  Undoubtedly commercial
pressures will tempt some contractors to maliciously exploit
soundness-related vulnerabilities, and so we should be taking steps now to
address this.  I'm sure there would have been many in 1970s/80s pooh-poohing
the risk of computer users exploiting security-related vulnerabilities.


on 30/1/12 11:51 AM, Lawrence Paulson <lp15 at> wrote:

> 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
> that this soundness guarantee is restricted to the inference core; for
> example, nothing prevents users from configuring the parser to parse
> 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.