50 Years of Proof Assistants
The article discusses the evolution of proof assistants over the past 50 years, highlighting the significance of Edinburgh LCF in the field. It outlines the foundational principles introduced by Edinburgh LCF and its impact on subsequent developments in proof technology. The author reflects on personal experiences and contributions to the field during this period.
- ▪Edinburgh LCF was first announced in 1975 at a conference on Proving and Improving Programs.
- ▪It introduced principles such as goal-directed proof and a structured system of theories.
- ▪The author contributed to the development of proof assistants, including a verification of the unification algorithm.
Opening excerpt (first ~120 words) tap to expand
50 years of proof assistants 05 Dec 2025 [ memories LCF HOL system Isabelle Coq Lean MJC Gordon Standard ML ] Crackpots ranging from billionaire Peter Thiel to random YouTube influencers claim that science has been stagnating for the past 50 years. They admit that computing is an exception: they don’t pretend that my personal 32GB laptop is not an advance over the 16MB mainframe that served the whole Caltech community when I was there. Instead they claim that advances in computing were driven solely by industrial research, quite overlooking the role of academia and government funding in pushing the VLSI revolution, RISC processor design, networking, hypertext, virtual memory and indeed computers themselves.
…
Excerpt limited to ~120 words for fair-use compliance. The full article is at Github.
Discussion
0 commentsMore from Github
