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.
In C and C++ (where you don't have the >>> operator), you can do this:
6: mid = ((unsigned int)low + (unsigned int)high)) >> 1;
That so-called "fixed" code just couldn't do anything useful in a 32-bit address space. A billion 32-bit ints completely fills up the address space by itself. As you note, perhaps it could "technically" be possible to search a billion 8-bit bytes, but that's not what's being passed in to the function.
And if he's running in a 64-bit address space (otherwise how could he pass in an array of a billion ints), then he should be using 64-bit integer arithmetic. (I don't know enough about Java to know how feasible it is to do that).
int mid = low + (high - low) / 2;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"
The implementer is not free of proving her implementation correct, given that the original algorithm was proven correct on some theoretical computational model. Bloch argues that, since the original proof is not sufficient, the implementer needs to test. I'd add, that if the implementer would adapt/redevelop the proof for her implementation, she might forgo testing. Of course, this is practically impossible for many execution environments.
If you forget/omit a single fact about your target platform/machine/api (whatever axioms you found your reasoning on) in your proof, it may be worth nothing.