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

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 Paulson

> On 11 Dec 2016, at 23:19, Randy Pollack <rpollack at> 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.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.