[SystemSafety] Fetzer

[Derek M Jones]

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/

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