9
$\begingroup$

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.

Improve this question
$\endgroup$
  • 6
    $\begingroup$ This is why we have techniques to prove correctness of algorithms, even if (correct) implementation on a real machine is hard. $\endgroup$ – Raphael Jan 24 '11 at 10:42
  • 9
    $\begingroup$ 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. $\endgroup$ – Tsuyoshi Ito Jan 24 '11 at 11:45
  • 8
    $\begingroup$ 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. $\endgroup$ – Peter Shor Jan 24 '11 at 12:31
  • 2
    $\begingroup$ 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. $\endgroup$ – Kaveh Jan 24 '11 at 13:38
  • 5
    $\begingroup$ "Beware of bugs in the above code; I have only proved it correct, not tried it." ~Donald Knuth $\endgroup$ – Lev Reyzin♦ Jan 25 '11 at 14:07
11
$\begingroup$

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?")

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.