I love this line from Donald Knuth:
Beware of bugs in the above code; I have only proved it correct, not tried it.
He wrote this in 1977, at the end of a memo on van Emde Boas priority deques.
The word only makes it. He had proved the code correct. He hadn’t run it yet.
A good reminder to test things, even when we think we have them figured out. A proof depends on its assumptions. We can miss something in the argument or make a mistake in the code. Tests can miss things too. I like having both.
I was also curious about the language. It looks like ALGOL-style pseudocode. I wouldn’t call it a specific dialect from this excerpt alone. Here is the little procedure above the quote:
procedure insert2 (integer x, ℓ)
begin B[ℓ] ← B[ℓ] ∨ (2 ↑ (x mod 16));
size[ℓ] ← size[ℓ] + 1;
if x < least[ℓ] then least[ℓ] ← x
else if x > greatest[ℓ] then greatest[ℓ] ← x;
end;
The arrows take a moment to get used to. ← means assignment. ↑ means exponentiation. ∨ is bitwise OR here.
Sources: Knuth’s account and the original correspondence.