[byerley]

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"

[kagebe]

Well, then I restate: "Those proofs were not proofs of the theorems they/Bloch wanted to prove." The point being: Proving is not just about your proof, but also about writing meaningful Theorems, or as it is more commonly called when programming: specification.

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.