[SystemSafety] Fetzer

[Nick Tudor]

Just to add, the LCF style theorem provers have, to my knowledge, never had
an unsoundness shown in them...despite a huge amount of use in various use
cases from academia to industrial scale.  We used one  - ProofPower to do
the independent verification of all Typhoon FCS software - 350,000
SLOC....we found a < when it should have been a <=....same day the test
pilot found it (ie a test) which meant that the aircraft didn't respond to
a demand AKA a trouser filling experience.  This was after an awful lot of
ground based test.  Other examples are available for how FM and maths has
found stuff that test never would....and vice versa (because FM are not the
appropriate tool).

Nick Tudor
Tudor Associates Ltd
Mobile: +44(0)7412 074654
www.tudorassoc.com

*77 Barnards Green Road*
*Malvern*
*Worcestershire*
*WR14 3LR*
*Company No. 07642673*
*VAT No:116495996*

*www.aeronautique-associates.com <http://www.aeronautique-associates.com>*


On Wed, 19 Jun 2019 at 14:46, David Crocker <dcrocker at eschertech.com> wrote:

> 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/
> >
> >
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
> Manage your subscription:
> https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20190619/29a89e6d/attachment.html>