On 10/4/2014 3:24 PM, Nick Sabalausky wrote:
On 10/04/2014 06:20 PM, Nick Sabalausky wrote:
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.
Yup. Proofs are just another tool that helps, not a magic solution.
