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



This is good if the proof scripts are readable and can then be read over by mathematicians for added assurance. But it doesn't really help in cases where the formal proof uses highly automated steps, like in much of Flyspeck, especially in the parts of Flyspeck where linear and non-linear inequalities are dealt with.

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 Paulson


On 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.




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