50 years of proof assistants
Summary
This post provides a 50-year retrospective on proof assistants, tracing the evolution from Edinburgh LCF through HOL/Isabelle to Rocq and Lean. It highlights major milestones in formal verification, including hardware verification (seL4), verified compilers (CompCert, CakeML), and the growing mainstream adoption of formal methods in mathematics and industry, while acknowledging ongoing challenges and future directions.