On 10/04/2014 06:20 PM, Nick Sabalausky wrote:
On 10/04/2014 03:57 PM, Ola Fosheim Grostad wrote:
A validated correctness proof ensures that the code follows the
specification, so no bugs.
The day we can guarantee a correctness proof as being perfectly sound
and...well...correct is the day we can guarantee software correctness
without the formal proof.
Proofs are just as subject to mistakes and oversights as actual code.
Proofs deal with that via auditing and peer review, but...so does
software. It sure as hell doesn't guarantee lack of bugs in software, so
what in the world would make anyone think it magically guarantees lack
of mistakes in a "proof"? (A "proof" btw, is little more than code which
may or may not ever actually get mechanically executed.)
And the "specification" itself may have flaws as well, so again, there
are NO guarantees here whatsoever. The only thing proofs do in an
engineering context is decrease the likelihood of problems, just like
any other engineering strategy.
