Your type checker may be wrong - an introduction to formal proof verification and the Curry-Howard Correspondence
Summary
The post introduces the Curry-Howard correspondence and explains how proof assistants use type systems to verify proofs. It discusses the limits of type checkers, the halting problem, and Gödel’s incompleteness, arguing that even rigorous systems can be provably imperfect. The piece uses Lean-like reasoning to illustrate how proofs map to programs and what this means for developers using formal verification tools.