*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Fwd: soundness of Isabelle/HOL*From*: Randy Pollack <rpollack at inf.ed.ac.uk>*Date*: Mon, 30 Jan 2012 09:56:29 -0500*In-reply-to*: <CANofLeJCtnVRTW82ipVPi7Rim7h=3-E8o5tXAKCY3tJOyJEGwQ@mail.gmail.com>*References*: <1327928344605@names.co.uk> <CANofLeJCtnVRTW82ipVPi7Rim7h=3-E8o5tXAKCY3tJOyJEGwQ@mail.gmail.com>*Sender*: rpollack0 at gmail.com

---------- Forwarded message ---------- From: Randy Pollack <rpollack0 at gmail.com> Date: Mon, Jan 30, 2012 at 9:50 AM Subject: Re: [isabelle] soundness of Isabelle/HOL To: "\"Mark\"" <mark at proof-technologies.com> Cc: lp15 at cam.ac.uk, Matthias.Schmalz at inf.ethz.ch, cl-isabelle-users at lists.cam.ac.uk A well known approach to soundness, not discussed here yet, is independent checking. As Larry points out, a user must read and understand the statements of theorems s/he wants to believe, and all definitions they hereditarily depend on. Further there must be confidence that whatever form these theorems are presented in is correctly captured by a proof tool's internal representation (issues of printing/parsing/overloading, etc). But the actual proofs are no cause to worry, at least in principle, at least in a system like Coq or Isabelle that can produce complete, independently checkable proof scripts. in some completely unambiguous notation. Randy Pollack -- On Mon, Jan 30, 2012 at 7:59 AM, "Mark" <mark at proof-technologies.com> wrote: > 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. > > Mark. > > on 30/1/12 11:51 AM, Lawrence Paulson <lp15 at cam.ac.uk> 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 > 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 >>> >> >> >> >> > >

**References**:**Re: [isabelle] soundness of Isabelle/HOL***From:*"Mark"

- Previous by Date: [isabelle] WING 2012: First Call for Papers
- Next by Date: [isabelle] graph theory in isabelle - nominal?
- Previous by Thread: Re: [isabelle] soundness of Isabelle/HOL
- Next by Thread: Re: [isabelle] Fwd: soundness of Isabelle/HOL
- Cl-isabelle-users January 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list