Skip to content(if available)orjump to list(if available)

50 years of proof assistants

50 years of proof assistants

2 comments

·December 12, 2025
Visit

ratmice

I wish he had just said 50 years of LCF, since he even mentions automath in the article but that was but that was late 60s

Animats

> In 1994, came the Pentium with its FDIV bug: a probably insignificant but detectable error in floating-point division. The subsequent product recall cost Intel nearly half a billion dollars. John Harrison, a student of Mike’s, decided to devote his PhD research to the verification of floating-point arithmetic.

No mention of the effort by Boyer and Moore, then at their Computational Logic, Inc., to do a formal verification of the AMD FPU for the AMD5K86TM. The AMD chip shipped with no FDIV bug. [1]

[1] https://dl.acm.org/doi/abs/10.1109/12.713311