[SystemSafety] Number Theorist Fears All Published Math Is Wrong

[Derek M Jones]

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