[SystemSafety] Number Theorist Fears All Published Math Is Wrong

[Derek M Jones]

David,

> Have you every actually used a tool that attempts to provide formal
> proof of software correctness? If so, how many demonstrably false

"formal proof of software correctness" is a meaningless marketing term.

There are tools that show:

    o for specified input, a specified list of expressions are true,

    o that it was not possible to find any inconsistencies between
a specification and code claiming to implement the specification.

These tools fail to find faults, just like testing.

The open question is the extent to which they might, or might
not be more cost effective than testing.


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