*To*: Peter Lammich <lammich at in.tum.de>*Subject*: Re: [isabelle] Verify the legitimacy of a proof?*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Mon, 10 Jul 2017 18:40:38 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1499677854.8165.12.camel@in.tum.de>*References*: <CADYF24fBE5-wFje-T9-z2c9Um4ZGf1y+ukaSiDi3EPa9uRBEaw@mail.gmail.com> <5b1c5907-c172-0e3d-6163-c70e0bc884c7@sketis.net> <CADYF24c9L7mdmpNspoSEinHGU-V-_w1axhYvsHqO4_cMnRhxnw@mail.gmail.com> <BD9ECBCD-B093-4F5F-91E1-8BF6714337B3@cam.ac.uk> <1499677854.8165.12.camel@in.tum.de>

I think that we are talking at cross purposes here. Of course we want our systems to be sound, and a kernel architecture is a great help in this, as we have known for 40 years. But even with a kernel architecture, it is easy for a result to be misrepresented. See e.g. > Avra Cohn. The Notion of Proof in Hardware Verification. J. Autom. Reasoning5(2): 127-139 (1989) The proof kernel is no defence whatever against misrepresentation or misunderstanding, so itâs important that formal documents are openly available for inspection. Larry Paulson > On 10 Jul 2017, at 10:10, Peter Lammich <lammich at in.tum.de> wrote: > > On Sa, 2017-07-08 at 19:59 +0100, Lawrence Paulson wrote: >> "We have been given a proof of X; Is it credible?" > > At this point, I second Ken. Although having human-readable machine > checked proofs is certainly a nice feature to get an idea of how a > proof works, the main points to check should be the statement of the > theorem, including the definitions (syntax tweaks, etc) it uses, as > well as the axioms its proof uses. Then, one relies on the logical > inference kernel that the proof is actually correct. > In particular, auxiliary lemmas and definitions only used for the > proof, but not in the main statement of the theorem, should be > irrelevant for trusting the theorem. > > This principle should, in first place, be independent of whether the > user is malicious or not. However, in Isabelle, the malicious user has > a lot of possibilities to hide tweaks from a reviewer, while, in > HOLZero, these possibilities are very limited (if existent at all). > > > Actually, Isabelle contains many tools in this spirit, for example, > even the simplifier or classical reasoner apply some transformations on > the theorems provided to them. More high-level tools like function > package or datatype package even do really complex proofs, completely > hidden from the user. > > -- > Peter > >

**Follow-Ups**:

**References**:**[isabelle] Verify the legitimacy of a proof?***From:*scott constable

**Re: [isabelle] Verify the legitimacy of a proof?***From:*Makarius

**Re: [isabelle] Verify the legitimacy of a proof?***From:*scott constable

**Re: [isabelle] Verify the legitimacy of a proof?***From:*Lawrence Paulson

**Re: [isabelle] Verify the legitimacy of a proof?***From:*Peter Lammich

- Previous by Date: Re: [isabelle] State of the State Monad
- Next by Date: Re: [isabelle] State of the State Monad
- Previous by Thread: Re: [isabelle] Verify the legitimacy of a proof?
- Next by Thread: [isabelle] Proof kernel, Pollack-consistency and faithfulness â Re: Verify the legitimacy of a proof?
- Cl-isabelle-users July 2017 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