[SystemSafety] Fetzer

[Derek M Jones]

David,

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

This approach is essential N-version programming, with N=2.

Two programs get written, one is nominated to be the specification,
and a tool checks that the behavior of the two programs are consistent
with each other.

The correctness argument relies on a verbal slight of hand.  The
program nominated to be the specification is deemed to be correct,
because it's the specification.  If the second program has consistent
behavior, compared to the 'specification', then it's said to be correct.

> 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

There is a lot more to consider than the error rate of the tool.

Particular tools are based on particular mathematical formalisms.  Which
means they are not capable of detecting inconsistencies of a kind not
supported by the formalism used, i.e., they look for a specific kind
of inconsistency.

As with all N-version solutions, the same incorrect behavior can occur
in both programs being compared.

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

-- 
Derek M. Jones           Software analysis
tel: +44 (0)1252 520667  blog:shape-of-code.coding-guidelines.com