*To*: Lawrence Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] [isabelle-dev] Circular reasoning via multithreading seems too easy*From*: Mark Adams <mark at proof-technologies.com>*Date*: Tue, 13 Dec 2016 01:15:22 +0700*Cc*: Markus Wenzel <makarius at sketis.net>, Randy Pollack <rpollack at inf.ed.ac.uk>, Julius Michaelis <j.michaelis at liftm.de>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <B8B560EC-F943-453D-B534-9D88497B2503@cam.ac.uk>*References*: <1480773469.4580.15.camel@in.tum.de> <cff246c2-779c-6f38-71f0-917ea473c9bc@sketis.net> <20161211215724.GA22532@liftm.de> <6a185f77-b9d5-31dc-0211-9acbce8bca84@sketis.net> <aa5f09e0-fe5d-4983-5a28-4831b3162702@sketis.net> <CANofLeJ99AM-TRNtd4RCahr8RSPnuFxOR0EphOy3=s9PUOD0Ww@mail.gmail.com> <B8B560EC-F943-453D-B534-9D88497B2503@cam.ac.uk>*User-agent*: Roundcube Webmail/1.2.1

Mark. On 13/12/2016 00:00, Lawrence Paulson wrote:

There is a totally different way of looking at correctness. It doesnât replace technical means (proof kernels, separate checkers), but complements them. It is to make the proof readable to humans as well as to machines, so that a particular proof can be can be inspected by a mathematician using no tools but the human eye. From the point of view of many mathematicians, reliance on computers introduces too much uncertainty. They worry not only about subtle bugs in the code (even if confined to a kernel of a few hundred lines) but about cosmic rays and the like. I find this point of view extreme, but it is there. With such a point of view, even a fully bootstrapped verification of the prover implementation on a verified compiler may be suspect, because the proof itself will look to such a sceptic as nothing but thousands and thousands of lines of additional code. Here the legibility of the proof itself offers a different type of confidence. If the premises and conclusion of the theorem are clear, and the correctness of each step (shown by explicit intermediate assertions, for example using âhaveâ) can be verified by inspection, then a mathematician can be convinced by such a proof independently of what may be going on in the machine. It is of course possible that the mathematicianâs interpretation of the proof (and even the formal language it was written in) might deviate from the intended meaning. Larry PaulsonOn 11 Dec 2016, at 23:19, Randy Pollack <rpollack at inf.ed.ac.uk> wrote: Absolute certainty cannot be obtained by millions of lines of code (prover, compiler, OS, ...) running on real hardware, but, as Hugo points out, independent checking goes some ways toward improved confidence. Truly independent checking is asking a lot of a reader of a formal development, but Coq has stand-alone coqchk; some HOLs can be checked by HOL-zero.

**References**:**Re: [isabelle] [isabelle-dev] Circular reasoning via multithreading seems too easy***From:*Makarius

**Re: [isabelle] [isabelle-dev] Circular reasoning via multithreading seems too easy***From:*Makarius

**Re: [isabelle] [isabelle-dev] Circular reasoning via multithreading seems too easy***From:*Randy Pollack

**Re: [isabelle] [isabelle-dev] Circular reasoning via multithreading seems too easy***From:*Lawrence Paulson

- Previous by Date: Re: [isabelle] [isabelle-dev] Circular reasoning via multithreading seems too easy
- Next by Date: [isabelle] Random term given its type
- Previous by Thread: Re: [isabelle] [isabelle-dev] Circular reasoning via multithreading seems too easy
- Next by Thread: Re: [isabelle] [isabelle-dev] Circular reasoning via multithreading seems too easy
- Cl-isabelle-users December 2016 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