Program logic bugs vs input/environmental errors

[Walter Bright via Digitalmars-d]

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.