[Open-graphics] [OT] Nicolas Capens an impolite member ?

Nicolas Capens nicolas at capens.net
Sun Dec 12 18:04:10 EST 2004


Hi Viktor,

> ROTFL

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
>> make
>> 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
implementation.

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

Kind regards,

Nicolas 




More information about the Open-graphics mailing list