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.
Several years ago, there has been a (rather harsh) debate on a topic similar to this. It all started when several complex proofs turned out to be incorrect, and some researchers started to raise doubts on the very nature of proofs (well, I should have said "provable cryptography," but for the sake of generality, I didn't). Both sides of the controversy accused the other to misunderstand the concepts. Here's a link for more info.

Proofs are our (mathematical) tools to prove theorems/algorithms are correct, but when they became too complex, we may slip and prove wrong things to be right. The recent 100-or-so-page proof on P≠NP is an excellent example. However, this does not rule out the very nature of proofs: Nothing's wrong with them.

One last point: I think studying the philosophy of science will give us more insight on this. (Under the given link, see the bullet "How do we know whether a mathematical proof is correct?")