*To*: Lawrence Paulson <lp15 at cam.ac.uk>, scott constable <sdconsta at syr.edu>*Subject*: Re: [isabelle] Verify the legitimacy of a proof?*From*: Lars Hupel <hupel at in.tum.de>*Date*: Sat, 8 Jul 2017 21:43:36 +0200*Cc*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>, Makarius <makarius at sketis.net>*In-reply-to*: <BD9ECBCD-B093-4F5F-91E1-8BF6714337B3@cam.ac.uk>*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>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.2.1

> However, we work with formal proofs, which can be examined, even > interactively. We do not have to work on the basis that "X has been > proved, therefore X is true", but rather "We have been given a proof > of X; Is it credible?" Then we can look at any part of this proof > where we have doubts. A devious user has many ways to try to fool us, > but it's not so easy if he has to supply the full source code and we > insist on legibility throughout. The effort we choose to invest in > this would depend on how important X is and how much we distrust the > person who supplied the proof. Maybe it's time for an Underhanded Isabelle Contest? <http://www.underhanded-c.org/> <https://en.wikipedia.org/wiki/Underhanded_C_Contest> Cheers Lars

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

- Previous by Date: Re: [isabelle] Verify the legitimacy of a proof?
- Next by Date: Re: [isabelle] Verify the legitimacy of a proof?
- Previous by Thread: Re: [isabelle] Verify the legitimacy of a proof?
- Next by Thread: Re: [isabelle] 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