Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Nearly all binary search and merge sort implementations are broken (2006)

googleresearch.blogspot.com

Post reply on HN
Print view View original

51–60 of 70 posts

Re: Nearly all binary search and merge sort implementations are broken (2006)

#51

Post by 6ren »

adrianN wrote: post #47
6ren wrote: post #31

Earlier quoted context omitted.

How do you prove the proof is correct? And how do you prove that your mathematical representation correctly corresponds to the problem you are modeling? This is why I am bitter and disillusioned about mathematics: it promises certainty, but doesn't deliver. It remains pragmatically useful, like many other tools, but does not deserve the semi-mystical status some confer on it.

The proof is a sequence of extremely easy logical inference rules like if A=>B and A then B. You check the correctness of the proof by verifying that these rules are applied correctly. Obviously though, there is no way to prove that your mathematical model corresponds to reality. That is because mathematics is not concerned with reality.

What if you make a mistake in checking the proof? Sure, that may sound silly, but mistakes are the point at issue here.

The usual rejoinder is that you can use an automated proof checker/assistant like COQ. Now you're relying on a program. Is the program correct? Well, we checked it with itself...

I admit this is far better than not having a proof at all. As I said, it's a tool, and has pragmatic merit. My objection is it's not absolute proof - which is what "proof" sounds like to me. In reality, a proof is an argument for the truth of a claim, with a level of convincingness.

BTW: Admittedly, reducing a proof to simple rules makes it harder to get wrong, though this is rarely done by mathematicians. Also, it's a curious fact that some mathematicians have made mistakes in their proofs, but turned out to be right anyway, presumably because they could see that it was true, and the notation was secondary.

Re: Nearly all binary search and merge sort implementations are broken (2006)

#52

Post by baddox »

jrockway wrote: post #16
DarkShikari wrote: post #8

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. This statement is tantamount to saying "you don't merely need to prove Fermat's Last Theorem, you also have to test it for all possible input values". By this line of reasoning, most of mathematics sho…

Mathematics sits atop a very small set of trusted axioms. Computer hardware is not so reliable; the parts are made in China as cheaply as possible. So even if you've proven something correct in theory, it doesn't matter because of all the additional variables that the real world introduces. The big insights in computer science look very much like mathematics; the mechanics of a binary search work perfectly in theory.…

It seems like you can only prove something in computer software up to the point of some random failure in hardware. If there's a chance that a cosmic ray will randomly flip a bit in memory every quintillion clock cycles, then surely you can only prove that an algorithm is correct with the explicit concession that it might be wrong every decade or so.

Re: Nearly all binary search and merge sort implementations are broken (2006)

#53

Post by mrich »

finnw wrote: post #42
Wilduck wrote: post #5

An interesting article that links back to this one: http://reprog.wordpress.com/2010/04/19/are-you-one-of-the-10... The claim is that even ignoring overflow, only 10% of programmers can correctly implement a binary search. When I tried it, I thought I got it working, but it was later pointed out that I didn't handle empty lists correctly. Programming correctly is hard.

I hope that means "10% get it right first time" and not "only 10% can do it at all, even given a computer and a whole day to do it." Couldn't resist that challenge (although the thread is nearly 2 years old.) I think mine works, at least it gives the right answer for all my test cases.

It's even hard to come up with all the relevant test cases - if you miss a corner case in the implementation, it is likely you will oversee it also in the test case generation. Only an exhaustive search would somehow be able to discover this.

With e.g. templates in C++, this is possible in some cases. You can test a template version using the limited range of an unsigned char, while your real implementation will use a uint64.

But instead of implementing e.g. a binary search, I prefer to take a proven implementation from e.g. the STL and adapt it for my needs. Experience and programmer lazyness have taught me this is a good way :)

Re: Nearly all binary search and merge sort implementations are broken (2006)

#54

Post by baddox »

nazgulnarsil wrote: post #24
DarkShikari wrote: post #23

Earlier quoted context omitted.

You are making a categorical error: One proves algorithms and tests programs. You can prove programs too, not just algorithms. That's what the entire (exorbitantly expensive) field of verified applications lies upon. Even my college class on formal logic covered the basics of this, and there's billions of dollars worth of extremely high-reliability applications that have been developed using such formal proofs. For e…

you can prove theoretical programs. do you really want to have to prove that it still works with any random bit flipped at runtime? what about two random flipped bits?

You're challenging what it means for something to be a proof, which I think is always subject to philosophical debate. Intuitively, something is a proof of a proposition if it convinces someone else that the proposition is true, and the proposition actually is true.

Obviously, for difficult concepts, it's possible that every expert in the world could be convinced that a proposed proof is correct, only to later find out that it's not. The way I see it, you're always only proving that something has a high probability of being correct, and showing how high the probability is. For computer software, you might be showing that your program is correct with the same probability that the underlying hardware is working as specified (so cosmic rays shifting bits or faulty hardware are possible exceptions baked into your proof).

To get a bit silly, a mathematical proof delivered from person A to person B is really only showing that a proposition is true with the same probability that person B is sane, educated, and is understanding the concepts correctly,

Re: Nearly all binary search and merge sort implementations are broken (2006)

#55

Post by yason »

I don't like the index variables and splitting in half part. I like to write my binary searches with bit patterns:

1) figure out the number of bits required to cover the largest index (= a little bit of cheap bit-twiddling)

3) initialize your index to 0

2) flip a bit on in index, starting from the highest bit available from step 1)

3) if data[index] is smaller than what you're looking for, leave the bit on

4) try with the next-lowest bit and loop to 2) until at bit #0

It's pretty easy to write it out in a way that's just obvious, instead of requiring the reader to wrap his mind about which variable is the lowest and highest bound and whether the indexes are inclusive/exclusive in which ends, etc.

Re: Nearly all binary search and merge sort implementations are broken (2006)

#56

Post by gradstudent »

6ren wrote: post #51
adrianN wrote: post #47

Earlier quoted context omitted.

The proof is a sequence of extremely easy logical inference rules like if A=>B and A then B. You check the correctness of the proof by verifying that these rules are applied correctly. Obviously though, there is no way to prove that your mathematical model corresponds to reality. That is because mathematics is not concerned with reality.

What if you make a mistake in checking the proof? Sure, that may sound silly, but mistakes are the point at issue here. The usual rejoinder is that you can use an automated proof checker/assistant like COQ. Now you're relying on a program. Is the program correct? Well, we checked it with itself... I admit this is far better than not having a proof at all. As I said, it's a tool, and has pragmatic merit. My objection…

If you make a mistake in checking the proof, the the proof is incorrect. The problem is with your application of the mathematics, not the applicability of mathematics itself to the problem of showing the truth of things.

Re: Nearly all binary search and merge sort implementations are broken (2006)

#57

Post by xyzzyz »

Confusion wrote: post #49
DarkShikari wrote: post #23

Earlier quoted context omitted.

You are making a categorical error: One proves algorithms and tests programs. You can prove programs too, not just algorithms. That's what the entire (exorbitantly expensive) field of verified applications lies upon. Even my college class on formal logic covered the basics of this, and there's billions of dollars worth of extremely high-reliability applications that have been developed using such formal proofs. For e…

The programs that can be proven are severely limited in power. For one, the tools to prove correctness of programs can't deal with data other than integers[1]. The way this usually works is that the proof is written and the code is then generated from the proof. That code is then incorporated in something larger, which has not been proven correct. Such is the case with algorithms. You can mathematically prove an algo…

For one, the tools to prove correctness of programs can't deal with data other than integers.

This is the first time I hear such claim. Which tools are you talking about? The tools I know (Coq) certainly don't have such limitations -- why would they, anyway?

Re: Nearly all binary search and merge sort implementations are broken (2006)

#59

Post by ColinWright »

yason wrote: post #55

I don't like the index variables and splitting in half part. I like to write my binary searches with bit patterns: 1) figure out the number of bits required to cover the largest index (= a little bit of cheap bit-twiddling) 3) initialize your index to 0 2) flip a bit on in index, starting from the highest bit available from step 1) 3) if data[index] is smaller than what you're looking for, leave the bit on 4) try wit…

That's really cool - would you care to post some example code so we can see the clarity obtained by this novel approach?

Did you come up with it yourself, or did you see it somewhere else?

Re: Nearly all binary search and merge sort implementations are broken (2006)

#60

Post by xyzzyz »

6ren wrote: post #51
adrianN wrote: post #47

Earlier quoted context omitted.

The proof is a sequence of extremely easy logical inference rules like if A=>B and A then B. You check the correctness of the proof by verifying that these rules are applied correctly. Obviously though, there is no way to prove that your mathematical model corresponds to reality. That is because mathematics is not concerned with reality.

What if you make a mistake in checking the proof? Sure, that may sound silly, but mistakes are the point at issue here. The usual rejoinder is that you can use an automated proof checker/assistant like COQ. Now you're relying on a program. Is the program correct? Well, we checked it with itself... I admit this is far better than not having a proof at all. As I said, it's a tool, and has pragmatic merit. My objection…

Proving theorems in mathematics plays a bit different role than proving correctness of programs. In mathematics, it's about sharing ideas, so if the proof is not completely correct, it can still be interesting because of the ideas and methods it uses. When you prove correctness of programs though, the whole point is to be sure that the program is correct, so the actual proof is important here, not its method or structure, because it's usually clear why the program at hand works.
Post reply on HN