# Powerful algorithms that are just too hard to implement— how to be sure they are right?

I am referring to the question here: powerful algorithms too complex to implement.

If an algorithm is powerful, but too complex to implement, how can you be sure that the algorithm is correct? Without implementation you won't be able to test the algorithm in a real world scenario, and such a complex algorithm can contain bugs, which may invalidate the algorithm.

This is what I do not understand; if you have the techniques to prove the correctness of an algorithm, then you would have the algorithm to implement it already, isn't it? Or else how can we be sure that the proving technique is correct?

I'm sorry if I sound elementary!

Update from Kaveh ( reproduced here because the argument is better!):

If you can formally prove the correctness of an algorithm in a formal system like Coq then you can also extract the algorithm (because essentially you have implemented the algorithm), but the key fact is that for most algorithms we don't give formal proofs of correctness for the algorithm, we use informal proofs of correctness. The proofs can be false, which does happen from time to time, and even a formal proof of correctness will not make us absolutely sure that the algorithm is correct.

• This is why we have techniques to prove correctness of algorithms, even if (correct) implementation on a real machine is hard. – Raphael Jan 24 '11 at 10:42
• I agree with Raphael. It appears that the question is based on an assumption that the correctness of an algorithm is usually proved by implementing it, but it is not the case. Proving the correctness of an algorithm and implementing an algorithm are completely different things, and one thing does not imply the other in either direction. – Tsuyoshi Ito Jan 24 '11 at 11:45
• Simple algorithms with complex proofs of correctness -- how do you know that they are right? Just because an algorithm works on test examples doesn't mean it works on all inputs. – Peter Shor Jan 24 '11 at 12:31
• I agree with most of the comments, but I think they are missing a key point. If you can formally prove the correctness of an algorithm in a formal system like Coq then you can also extract the algorithm (because essentially you have implemented the algorithm), but the key fact is that for most algorithms we don't give formal proofs of correctness for the algorithm, we use informal proofs of correctness. The proofs can be false, that does happen from time to time, and even a formal proof of correctness will not make us absolutely sure that the algorithm is correct. – Kaveh Jan 24 '11 at 13:38
• "Beware of bugs in the above code; I have only proved it correct, not tried it." ~Donald Knuth – Lev Reyzin Jan 25 '11 at 14:07