[isabelle] Fwd: soundness of Isabelle/HOL



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