[SystemSafety] Fetzer

[David Crocker]

Derek,

Of course large hand-constructed mathematical proofs are likely to
contain errors, just as any large body of program text that has not been
subject to independent verification is likely to contain errors. But
nobody constructs program proofs by hand these days, except perhaps in
academia. Formal proofs of programs are always constructed either
completely automatically, or in a few cases using an interactive theorem
prover.

So the important question is: what is the error rate of
machine-constructed program proofs, produced by whatever tool is used to
generate them. I think this is akin to asking what is the rate of code
generation bugs in a compiler. A "young" compiler that has not been used
very much may contain many errors, some of which will cause it to reject
valid input, others may cause it to terminate abnormally, and others
still will cause it to generate incorrect code. Similarly,  a "young"
program proof tool that has not been used much may contain many errors,
of which a only subset may lead to invalid "proofs" (our experience is
that the vast majority of prover bugs lead to rejecting valid input, or
to failing to prove things that should be trivial to prove). But as the
compiler or program verifier is used more and more, the serious bugs
(the ones that lead to code generation errors or incorrect proofs) are
uncovered; and after a greater of lesser amount of time the compiler or
verifier is reliable enough to be used in building critical software.
But neither a compiler nor a program verifier should be trusted
absolutely, which is one of the reasons why testing will always have an
important role.

Regards

David Crocker, Escher Technologies Ltd.
http://www.eschertech.com
Tel. +44 (0)20 8144 3265 or +44 (0)7977 211486

On 19/06/2019 13:54, Derek M Jones wrote:
> David,
>
> The idea that software can be proved correct is based on the
> assumption that mathematics is always correct.
>
> Plenty of mistakes get made in so called mathematical proofs.
> In some cases theorems are given with only an outline of a proof.
>
> And of course, a lot more people are running code, than checking
> mathematical proofs.  So more mistakes get found in code than
> mathematics.
>
> The continuing belief that mathematics can be used for proving
> software correct should be a fertile topic for social scientists
> and anthropologists, no need to visit 'primitive' tribes to
> find strange ideas, they are here under their noses.
>
> https://shape-of-code.coding-guidelines.com/2013/11/17/what-is-the-error-rate-for-published-mathematical-proofs/
>
>
> https://shape-of-code.coding-guidelines.com/2018/02/19/mathematical-proofs-contain-faults-just-like-software/
>
>