Re: [isabelle] Fwd: soundness of Isabelle/HOL



On independent checking, relevant projects (apart from HOL Zero) include
OpenTheory ( http://www.gilith.com/research/opentheory/) and dedukti (
http://www.lix.polytechnique.fr/dedukti/).

> On Jan 30, 2012 2:56 PM, "Randy Pollack" <rpollack at inf.ed.ac.uk> wrote:
>>
>> ---------- 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
>> >>>
>> >>
>> >>
>> >>
>> >>
>> >
>> >
>>




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