"Why don't you use dependent types?" (lawrencecpaulson.github.io)

The author traces a personal history with dependent types—from AUTOMATH and Martin-Löf’s type theory to the early implementation of Isabelle—and explains why, despite their expressiveness, dependent types were ultimately not adopted as Isabelle’s main engineering choice. He argues that proof objects, intrinsic to most dependent-type systems under Curry–Howard, are often unnecessary and wasteful: the LCF architecture (Robin Milner) uses a small trusted kernel and implementation-language type checking to enforce correctness without large proof objects. Isabelle instead standardised on higher-order logic (Isabelle/HOL) plus engineering features like axiomatic type classes and locales. The ALEXANDRIA project vindicated this choice by formalising deep mathematics (e.g., algebraically closed field extensions and the Balog–Szemerédi–Gowers theorem) without hitting a “dependent-types-only” barrier, even as systems like Lean showed massive community-driven success. For the AI/ML and theorem-proving communities the lesson is practical: dependent types give powerful encodings and links to program synthesis, but they carry trade-offs—performance issues, complications around intensional equality, evolving calculi and optional axioms, and trickier proof engineering. Tooling, libraries, automation and community momentum often matter as much as theoretical expressiveness. In short, dependent types are a valuable option, not an automatic win; pick the formalism based on the verification goals, ecosystem, and the engineering costs of automation and equality handling.