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.