[SystemSafety] Number Theorist Fears All Published Math Is Wrong
Derek M Jones
derek at knosof.co.uk
Wed Oct 30 13:45:11 CET 2019
Rod,
> I can think of several projects where some non-trivial proofs of
> correctness have been achieved against a formal specification. Most of
Claimed "proofs of correctness" (non-trivial or otherwise) are essential
N-version programming, with N=2.
Somebody write a program, and somebody writes another program.
One of the programs is labeled as a specification.
Some set of behaviors of the two programs are compared using some tool
(the exact behavior compared varies with tool used).
The behaviors are either the same, or different.
If the two behaviors are the same, it is not a proof of correctness.
It is a proof that both programs (with one labeled a specification)
have the same set of behaviors that the tool used is capable of
comparing.
--
Derek M. Jones Software analysis
tel: +44 (0)1252 520667 blog:shape-of-code.coding-guidelines.com
More information about the systemsafety
mailing list