<p>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 href="http://web.archive.org/web/20130120133248/http://www.sigcrap.org/2007/09/14/the-koblitz-controversy/" rel="nofollow noreferrer">a link for more info</a>.</p>

<p>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 <a href="http://tinyurl.com/2fvetuy" rel="nofollow noreferrer">recent 100-or-so-page proof on P≠NP</a> is an excellent example. However, this does not rule out the very nature of proofs: Nothing's wrong with them.</p>

<p>One last point: I think studying the <a href="http://en.wikipedia.org/wiki/Philosophy_of_science#Philosophy_of_mathematics" rel="nofollow noreferrer">philosophy of science</a> will give us more insight on this. (Under the given link, see the bullet "<strong>How do we know whether a mathematical proof is correct?</strong>")</p>

CC BY-SA 3.0
2011-01-24T23:59:02.097Z
2016-12-29T10:33:00.163Z
2016-12-29T10:33:00.163Z
Sadeq Dousti
<p>I am referring to the question here: <a href="https://cstheory.stackexchange.com/questions/4491/powerful-algorithms-too-complex-to-implement">powerful algorithms too complex to implement</a>.</p>

<p>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. </p>

<p>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?</p>

<p>I'm sorry if I sound elementary!</p>

<p>Update from Kaveh ( reproduced here because the argument is better!):</p>

<blockquote>
  <p>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.</p>
</blockquote>

CC BY-SA 2.5
2011-01-24T09:03:45.557Z
If it's too complex to implement, there'll be no implementations, so it's a moot point. Ignoring that, the techniques will be the same as usual: debugging and verification. Except that it will be a tedious activity, likely to be beyond the state of the art in those areas.
Dave Clarke
CC BY-SA 2.5
2011-01-24T10:42:55.077Z
This is why we have techniques to *prove* correctness of algorithms, even if (correct) implementation on a real machine is hard.
Raphael
CC BY-SA 2.5
2011-01-24T11:15:11.943Z
@Raphael, but this is what I do not understand; if you have the techniques to prove it, then you would have the algorithm to implement it already, isn't it?
Graviton
CC BY-SA 2.5
2011-01-24T11:43:28.363Z
You have the algorithm, but that doesn't mean that it is easy to implement.
Vinicius dos Santos
CC BY-SA 2.5
2011-01-24T11:45:17.020Z
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
CC BY-SA 2.5
2011-01-24T11:46:41.823Z
I think that the question is too elementary for this site.  Voted to [close it as off topic](http://meta.cstheory.stackexchange.com/questions/663/what-does-closed-as-off-topic-mean).
Tsuyoshi Ito
CC BY-SA 2.5
2011-01-24T12:03:47.183Z
I think the real question is what makes some algorithms much easier to prove correct than to implement.
Jouni Sirén
CC BY-SA 2.5
2011-01-24T12:16:14.893Z
@Graviton On paper, you have an *abstract* machine model (semantics) and often don't care about *data structures* very much. *Numeric effects* (floating point numbers, overflows, ...) are most often ignored. Or take an extreme example: given (false) assumptions, you can prove algorithms "correct" that can never be implemented. This is just the good old gap between theory and practice resp. the used techniques. You can use *non-constructive* techniques for proofs (e.g. by contradiction) but that won't help you implementing.
Raphael
CC BY-SA 2.5
2011-01-24T12:31:34.767Z
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 
CC BY-SA 2.5
2011-01-24T13:38:53.147Z
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
CC BY-SA 2.5
2011-01-24T13:40:40.430Z
@Kaveh, I think you summed up my argument in a succinct and perfect manner. I'll incorporate your part into the question.
Graviton
CC BY-SA 2.5
2011-01-24T13:42:12.147Z
I.e. there is no way to be absolutely sure that an algorithm is correct. (and even if it is correct, it does not mean that it will work with no problem in practice, the OS and the physical machine running the algorithm, ... can fault and cause the algorithm give incorrect results.)
Kaveh
CC BY-SA 2.5
2011-01-24T15:40:54.013Z
One of the examples given as answer to the other question was Risch's integration algorithm. Assuming Wikipedia to be roughly correct, the reason there is no complete implementation is that it relies on being able to check whether an expression is identically zero, which is really nasty when the expression can be built up from basic arithmetic and nth roots. So if one step in your algorithm says "if (E = 0) then ... else ..." it can be easy to prove that the transformation is correct but complex to implement the test. (This is a special case of Raphael's answer).
Peter Taylor
CC BY-SA 2.5
2011-01-25T12:32:14.397Z
Kaveh, I assumed a *proof* (i.e. correct), of course. A non-proof does never show anything, agreed. Fear of mistakes can not be an argument against proofs, otherwise TCS would be pretty pointless. By the way, we all missed one important point: Proving the correctness of a pen&paper algorithm is fine but does not imply the correctness of a given implementation. There are ways around that, but one has to be bear that in mind. Note that this also applies to the transformation step from source code to machine code.
Raphael
CC BY-SA 2.5
2011-01-25T12:32:31.947Z
A professor of mine used to joke that for any given iterative implementation of Quicksort found in any text book, there would be at least one mistake. So far I have not been able to prove him wrong.
Raphael
CC BY-SA 2.5
2011-01-25T14:07:51.550Z
"Beware of bugs in the above code; I have only proved it correct, not tried it." ~Donald Knuth
Lev Reyzin
<ds.algorithms><implementation>
Powerful algorithms that are just too hard to implement-- how to be sure they are right?
Graviton
# Powerful algorithms that are just too hard to implement-- how to be sure they are right?

(Asked by: username_0 on 2011-01-24)

I am referring to the question here: [powerful algorithms too complex to implement](https://cstheory.stackexchange.com/questions/4491/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.

**Tags:** ds.algorithms, implementation
> **Comments:**
> **username_1**: If it's too complex to implement, there'll be no implementations, so it's a moot point. Ignoring that, the techniques will be the same as usual: debugging and verification. Except that it will be a tedious activity, likely to be beyond the state of the art in those areas.  
> **username_2**: This is why we have techniques to *prove* correctness of algorithms, even if (correct) implementation on a real machine is hard.  
> **username_0**: @Raphael, but this is what I do not understand; if you have the techniques to prove it, then you would have the algorithm to implement it already, isn't it?  
> **username_3**: You have the algorithm, but that doesn't mean that it is easy to implement.  
> **username_4**: 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.  
> **username_4**: I think that the question is too elementary for this site.  Voted to [close it as off topic](http://meta.cstheory.stackexchange.com/questions/663/what-does-closed-as-off-topic-mean).  
> **username_5**: I think the real question is what makes some algorithms much easier to prove correct than to implement.  
> **username_2**: @Graviton On paper, you have an *abstract* machine model (semantics) and often don't care about *data structures* very much. *Numeric effects* (floating point numbers, overflows, ...) are most often ignored. Or take an extreme example: given (false) assumptions, you can prove algorithms "correct" that can never be implemented. This is just the good old gap between theory and practice resp. the used techniques. You can use *non-constructive* techniques for proofs (e.g. by contradiction) but that won't help you implementing.  
> **username_6**: 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.  
> **username_7**: 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.  
> **username_0**: @Kaveh, I think you summed up my argument in a succinct and perfect manner. I'll incorporate your part into the question.  
> **username_7**: I.e. there is no way to be absolutely sure that an algorithm is correct. (and even if it is correct, it does not mean that it will work with no problem in practice, the OS and the physical machine running the algorithm, ... can fault and cause the algorithm give incorrect results.)  
> **username_8**: One of the examples given as answer to the other question was Risch's integration algorithm. Assuming Wikipedia to be roughly correct, the reason there is no complete implementation is that it relies on being able to check whether an expression is identically zero, which is really nasty when the expression can be built up from basic arithmetic and nth roots. So if one step in your algorithm says "if (E = 0) then ... else ..." it can be easy to prove that the transformation is correct but complex to implement the test. (This is a special case of Raphael's answer).  
> **username_2**: Kaveh, I assumed a *proof* (i.e. correct), of course. A non-proof does never show anything, agreed. Fear of mistakes can not be an argument against proofs, otherwise TCS would be pretty pointless. By the way, we all missed one important point: Proving the correctness of a pen&paper algorithm is fine but does not imply the correctness of a given implementation. There are ways around that, but one has to be bear that in mind. Note that this also applies to the transformation step from source code to machine code.  
> **username_2**: A professor of mine used to joke that for any given iterative implementation of Quicksort found in any text book, there would be at least one mistake. So far I have not been able to prove him wrong.  
> **username_9**: "Beware of bugs in the above code; I have only proved it correct, not tried it." ~Donald Knuth  

---

## 1 answers

### Answer by username_10 on 2011-01-24. Score: 11 | Accepted answer

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](http://web.archive.org/web/20130120133248/http://www.sigcrap.org/2007/09/14/the-koblitz-controversy/).

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](http://tinyurl.com/2fvetuy) 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](http://en.wikipedia.org/wiki/Philosophy_of_science#Philosophy_of_mathematics) will give us more insight on this. (Under the given link, see the bullet "**How do we know whether a mathematical proof is correct?**")


---

