<story><title>Nearly all binary search and merge sort implementations are broken (2006)</title><url>http://googleresearch.blogspot.com/2006/06/extra-extra-read-all-about-it-nearly.html</url></story><parent_chain></parent_chain><comment><author>DarkShikari</author><text>&lt;i&gt;It is not sufficient merely to prove a program correct; you have to test it too. Moreover, to be really certain that a program is correct, you have to test it for all possible input values, but this is seldom feasible.&lt;/i&gt;&lt;p&gt;This statement is tantamount to saying &quot;you don&apos;t merely need to prove Fermat&apos;s Last Theorem, you also have to test it for all possible input values&quot;.  By this line of reasoning, most of mathematics should be thrown out.&lt;p&gt;If you&apos;ve proven a program correct, &lt;i&gt;it is correct for all input values&lt;/i&gt;, whether you have tested them or not.  If your proof ignores complexities such as the range of data values, it isn&apos;t a correct proof to begin with.  And yes, proving programs correct is often possible -- in fact, the highest levels of software verification actually require explicit proofs of correctness for much of the code; see  &lt;a href=&quot;http://en.wikipedia.org/wiki/Evaluation_Assurance_Level#EAL7:_Formally_Verified_Design_and_Tested&quot; rel=&quot;nofollow&quot;&gt;http://en.wikipedia.org/wiki/Evaluation_Assurance_Level#EAL7...&lt;/a&gt;</text></comment>
<story><title>Nearly all binary search and merge sort implementations are broken (2006)</title><url>http://googleresearch.blogspot.com/2006/06/extra-extra-read-all-about-it-nearly.html</url></story><parent_chain></parent_chain><comment><author>ColinWright</author><text>Previous, extensive discussion: &lt;a href=&quot;http://news.ycombinator.com/item?id=1130463&quot; rel=&quot;nofollow&quot;&gt;http://news.ycombinator.com/item?id=1130463&lt;/a&gt;&lt;p&gt;I once ran a programming challenge based on this, but I discontinued when I started to get threats of physical violence from people whose code didn&apos;t pass the tests.&lt;p&gt;The Dictionary of Algorithms and Data Structures on the NIST site has a correction I submitted on exactly this point:&lt;p&gt;&lt;a href=&quot;http://xlinux.nist.gov/dads/HTML/binarySearch.html&quot; rel=&quot;nofollow&quot;&gt;http://xlinux.nist.gov/dads/HTML/binarySearch.html&lt;/a&gt;&lt;p&gt;And my blog post: &lt;a href=&quot;http://www.solipsys.co.uk/new/BinarySearchReconsidered.html?HN&quot; rel=&quot;nofollow&quot;&gt;http://www.solipsys.co.uk/new/BinarySearchReconsidered.html?...&lt;/a&gt;</text></comment>