Why Lean Is a Perfectable Language: Dependent Types, Metaprogramming, and Community Gravity

The author argues Lean stands apart because it is perfectable rather than perfect. You can state and prove properties about Lean code inside Lean itself, which collapses the traditional gap between programs and reasoning about them. Most languages eventually grow types, push computation into compile time, and accrete theorem-proving-like facilities piecemeal. Lean starts with dependent types and a real proof infrastructure, so that accumulation of guarantees, which the author calls progress, is native rather than bolted on.

On the syntax side, Lean’s metaprogramming is unusually seamless. The post walks through a tic-tac-toe example that introduces custom syntax categories and an elaborator to turn a visual board literal into a validated Board value at compile time, demonstrating how APIs can be layered and hidden behind bespoke notation. Combined with the ability to prove two pieces of code equivalent, this gives the compiler substantial optimization headroom, even if Lean is not yet Rust-fast, and makes aggressive refactoring tractable.

The final argument is sociological. Powerful metaprogramming usually triggers the Lisp curse of fragmented, half-finished projects, but formalizing mathematics is hard enough to force collaboration, and mathlib has become the shared cathedral. With Leo de Moura, Terence Tao, and Peter Scholze anchoring direction and unified tooling around Lake, Elan, and Reservoir, Lean has the community gravity that Coq, Agda, Idris, and F* never sustained.