[SystemSafety] Bursting the formal methods bubble

[Derek M Jones]

Peter,

> He said that computer scientists had developed much better methods for writing rigorous proofs,
> namely formal methods, and recommended their use also in mathematics to avoid mistakes.

That is not how I interpret what Lamport said:
"Computer scientists are more willing to explore unconventional proof
styles. Unfortunately, I have found that few of them care whether they
have published incorrect results. They often seem glad that an error was
not caught by the referees, since that would have meant one fewer 
publication.
I fear that few computer scientists will be motivated to use a proof
style that is likely to reveal their mistakes. Structured proofs are
unlikely to be widely used in computer science until publishing
incorrect results is considered embarrassing rather than normal."

and what did he have to say about rigorous proofs?
"Writing a rigorous proof is harder than writing a sloppy one,
and lazy writers will find excuses to avoid doing it."

>> The mathematics we all learn in school/university has been around
>> long enough to be throughly checked, which gives people a skewed
>> view of mathematics.
> 
> Like John Kelley's (then) 30-year-old mistake, I suppose.

Now we agree that new mathematical 'proofs' often contain bugs,
can you tell me what the claims about formal methods proving
correctness actually mean.

Should we interpret these claims to mean:
"This software is correct, apart from the bugs we have not been able
to find"?

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