# Donald Knuth on bugs and proofs (2026-10-02)

**URL:** <https://pluralist.net/t/donald-knuth-on-bugs-and-proofs-2026-10-02/348>\
**Category:** Code Reading\
**Created:** [October 2, 2026, 7:00am UTC](https://pluralist.net/t/donald-knuth-on-bugs-and-proofs-2026-10-02/348 "2026-10-02T07:00:00Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![delyan](https://pluralist.net/user_avatar/pluralist.net/delyan/32/245_2.png) [@delyan](https://pluralist.net/u/delyan)\
**Post date:** [October 2, 2026, 7:00am UTC](https://pluralist.net/t/donald-knuth-on-bugs-and-proofs-2026-10-02/348/1 "2026-10-02T07:00:00Z")

</div>

Brilliant quote from [Donald Knuth](https://en.wikipedia.org/wiki/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](https://11011110.github.io/blog/2010/01/14/van-emde-boas.html).

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](https://en.wikipedia.org/wiki/Simula) grew out of [ALGOL 60](https://en.wikipedia.org/wiki/ALGOL_60), which explains the resemblance. Here is the procedure above the quote:

```plaintext
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](https://cs.stanford.edu/~knuth/faq.html). He gives the date and the story behind the memo.
- [Scans of the original memo and correspondence](https://staff.fnwi.uva.nl/p.vanemdeboas/knuthnote.pdf). 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](https://www.softwarepreservation.org/projects/ALGOL/manual/NR_report_743_Dahl_Myhrhaug_Nygaard_Simula-67-Common-Base-Language.pdf). The language report, for a deeper look at SIMULA.
- [van Emde Boas trees, explained by David Eppstein](https://11011110.github.io/blog/2010/01/14/van-emde-boas.html). Background on the data structure.