[Open-graphics] [OT] Nicolas Capens an impolite member ?
nicolas at capens.net
Sun Dec 12 18:04:10 EST 2004
Not very polite of you...
> Bart van Leeuwen wrote:
>> There are 2 problems with this:
>> 1. While you can prove the correctness of an algorithm, that does nit yet
>> an implementation of one bugfree.
> One doesn't prove the correctness of an abstract algorithm. One proves the
> correctness of an algorithm written in a formal language, e. g. Java,
> Assembly or Verilog. As far as correctness proofs go, there is no
> difference between an algorithm and its implementation.
I agree with Bart. You can mathematically proof the correctness of an
abstract algorithm, but you can't prove the correctness of the
implementation. Even if you perfectly mapped an algorithm to a programming
language, there's no guarantee it's bug-free. You'd also have to prove your
compiler is flawless, the dependent libraries you use are flawless, the O.S.
works entirely as
expected, and the hardware has no errata. It's all part of the
I also think it's important to note the difference between 'correct' and
'bugfree'. Algorithms can be proven to be correct. Implementations can be
made of correct algorithms but still contain bugs. It can even execute
correctly but still contain bugs. Also, a correct implementation of an
incorrect algorithm can be bugfree. ;-)
More information about the Open-graphics