[SystemSafety] Number Theorist Fears All Published Math Is Wrong

[Derek M Jones]

Steve,

> While I do not, unfortunately, have objective, independent, quantitative
> data to support the value of software proofs of correctness, I would like

I am saying that proofs of correctness don't exist, only evidence that
certain kinds of behavior have not been found.

As Martyn pointed out, some tools are capable of providing evidence
of certain characteristics under a very wide range of circumstances,
e.g., absence of any fixed-point overflow.

> to offer the following qualitative argument for why it should be taken a
> lot more seriously than it is.

My argument centers around cost benefit.

Show a worthwhile cost/benefit for a technique, and I'm sure lots of
people will take it more seriously.

>    Depending on testing alone to reveal software defects‹to demonstrate
> code correctness‹is a hopelessly lost cause

"code correctness" is a marketing term.

But in general, relying on any one technique can often be a lost cause.


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