Nearly All Binary Searches and Mergesorts are Broken (2006)

Not that it detracts from your point, but the phrase is a reference to a famous Knuth quote:

http://www-cs-faculty.stanford.edu/~knuth/faq.html (see the last question)

Computers are now complicated enough for Computer Science to have turned to some extent into an empirical science - it is impossible for a single person to have in their head everything that goes in a typical computer, operating system, compiler and so forth, so one is often forced to resort to experiment to find things out, it's no longer a theory where you can just reason things out, maybe it never was one in fact, because many simple imperative programs are so complex to reason about.

In empirical sciences, you not only have to have a mathematically valid theory, but you also have to check if the theory fits reality by making predictions and experimentally checking them with the real world. It's the same now in Computer Science, there are so many places where theoretical assumptions might deviate from reality that having a proof is not enough. In fact, you have to have those assumptions to make things mathematically tractable. Imagine mathematicians or computer scientists re-proving real analysis theorems using floating point arithmetic...

In other words, your vision of proofs being enough as long as all the assumptions are part of the theory, seems utopian to me. In fact, even some of the most devoted advocates of correctness proofs have admitted this:

http://www.gwern.net/docs/1996-hoare.pdf

I do agree with the quoted statement. I have a lot of experience with machine-verified proofs (in a language called Coq). Even though Coq guarantees that an accepted proof is correct, you still can't necessarily trust it, because your formal model of the program may be not accurate enough, or your statement of correctness is improperly stated.

In this case, it seems like their proof was correct with respect to their model, but their model did not match up with reality. No amount of formalization will ever be able to solve this problem completely. I think the role of testing in this context is to make sure your formalization of the problem says what you meant to say about the world that you meant to refer to. Input/output examples (aka, tests) are a great way of convincing yourself of this.

>It is sufficient to prove a program correct - as long as your proof is not faulty!

This is unquestionable truth. Proof:

Proposition A(X): X is true in theory

Proposition B : For all X such that A(X), X is true in practice

Theoretically, there is no difference between theory and practice. ... (1)

Theoretically, statement B is true. [using (1)] ... (2)

Therefore, B is true in practice. [using (1) and (2)]

QED.

I would change it to "It is not sufficient merely to prove AN ALGORITHM IS correct; You have to test your implementation as well" ...

I am a PhD statistician and I can't understand your comment.

What statistic is being calculated for the N=1 Trillion dataset? And what is the way of calculating that would be off by 10%?

Yup.

More annoyingly, for a binary search over an array (i.e. something that can fit in memory) their code is still wrong - they should be using size_t.

As a theory guy I'd argue you're looking at it backwards.

The proofs are fine in that the correctness logically follows given the appropriate assumptions. In this particular example, it's implicitly assumed that integer overflow isn't a concern. Ideally, something like that should be explicitly stated, but let's be honest, Algorithms and Math in general have to be shorthand heavy - the alternative is painful and often not human readable.

It's always been the responsibility of the implementer to dive deep enough into the theory to grasp all the omitted assumptions. A less gratuitous headline might read - "Common implementation pitfalls: Integer Overflow"

Having an array with more than about 1.2 billion elements is all that it would have taken to break the old binary search, and that's not all that uncommon anymore.

Pure JavaScript code isn't vulnerable to integer overflow by virtue of not having any integer types, and I believe errors like this were the reason for leaving them out of the language.

> I would guess that nearly all code, period, is vulnerable to integer overflow issues.

Lack of checked integer arithmetic in some form is what I think is Java's biggest failure. Next to it is a lack of unsigned less/greater-than operator; it cannot be emulated easily with signed arithmetic. [There is unsigned right shift.]

(.Net _does_ have checked arithmetic; at least as an option.)

How so? From [1] it would seem that Lisps (idiomatic ones at least), Python, Perl, Haskell and Ruby are all free from the possibility of integer overflow. That definitely doesn't sound like "nearly all code".

[1] https://en.wikipedia.org/wiki/Arbitrary-precision_arithmetic

I see that as a limitation. "works only with data sizes up to half of MAXINT" is not a very surprising limitation of

     int mid = (low + high) / 2;

I was also thinking this was a stereotypical HN sensational headline blog post. Apart from being strangely correct, it somehow makes me want to code something in Java today.

> Python has a long integer type which won't over/underflow unless you run out of memory.

IIRC, so do Erlang, Ruby or Haskell (when using `Integer`), FWIW. And Java has BigInteger (though that one's a pain to use).

But there's a cost to their existence (they need to check for overflow at every operation), and a cost to going above machine word size. Also, now you've got "integers" which can take arbitrary amounts of memory and integer operations in O(n)

Still, definitely a plus on the correctness side.

There's also the option of type-encoded value ranges as in Pascal or Ada.

because Java arrays length is int, 32bit limited. I think we'll see these articles more and more :)