*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Verify the legitimacy of a proof?*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Sat, 8 Jul 2017 22:01:15 +0200*In-reply-to*: <CADYF24c9L7mdmpNspoSEinHGU-V-_w1axhYvsHqO4_cMnRhxnw@mail.gmail.com>*References*: <CADYF24fBE5-wFje-T9-z2c9Um4ZGf1y+ukaSiDi3EPa9uRBEaw@mail.gmail.com> <5b1c5907-c172-0e3d-6163-c70e0bc884c7@sketis.net> <CADYF24c9L7mdmpNspoSEinHGU-V-_w1axhYvsHqO4_cMnRhxnw@mail.gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:52.0) Gecko/20100101 Thunderbird/52.2.1

Scott,

Tobias On 08/07/2017 19:12, scott constable wrote:

Thanks all, I think this has been a productive discussion :) I would like to respond to a point Makarius brought up earlier: On 07/07/17 18:37, scott constable wrote:possibly written by other persons with malicious intentions.Isabelle does not protect against malicious intentions. It would require a quite different system to do that, one that you won't like to use. The other big provers (e.g. Coq) are similar in this respect. I'm also familiar with Coq, and I do think Coq should be better in this respect. In Coq, proofs are themselves objects with a given type. So they can be checked or examined, for instance by dumping them to the console. So to check the legitimacy of a theorem in Coq, I believe it would suffice to walk the proof tree by recursively expanding each non-atomic node, and thus ensure that the proof tree is composed entirely of legitimate proof objects. Am I wrong about this? If not, might there be a similar approach in Isabelle? Scott

**Attachment:
smime.p7s**

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

- Previous by Date: Re: [isabelle] Verify the legitimacy of a proof?
- Next by Date: [isabelle] primrec of datatype containing fset
- Previous by Thread: [isabelle] Proof kernel, Pollack-consistency and faithfulness â Re: Verify the legitimacy of a proof?
- Next by Thread: [isabelle] FW: Cl-isabelle-users Digest, Vol 145, Issue 3
- 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