Brilliant quote from Donald Knuth:
Beware of bugs in the above code; I have only proved it correct, not tried it.
Knuth wrote this in 1977, at the end of a memo on van Emde Boas priority deques.
The word only is key here - he proved the code correct but hadn’t run it yet. A proof depends on its assumptions. One can miss something in the argument or make a mistake in the code. Tests can miss things too. I like having both.
We were also curious about the language. The original memo answers that: Knuth calls it “SIMULA-like notation.” SIMULA grew out of ALGOL 60, which explains the resemblance. Here is the 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;
- arrows
←indicate assignment ↑is exponentiation∨is bitwise OR
The original pages are online too. They look typewritten, with underlined keywords and mathematical symbols. There is even a scan of the airmail envelope. We don’t know which machine was used or who did the typing.
Links to come back to:
- Knuth’s account of the quote. He gives the date and the story behind the memo.
- Scans of the original memo and correspondence. PDF page 2 has the envelope. Page 3 has the first page of the memo and the “SIMULA-like notation” sentence. Page 7 has the code and the famous warning.
- SIMULA 67 Common Base Language report. The language report, for a deeper look at SIMULA.
- van Emde Boas trees, explained by David Eppstein. Background on the data structure.