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.)
