At a party, Sydney Von Arx asked if I could name 40 programming languages. Yeah, that's the Bay for you. Racket, Agda, Clean, Elm, TypeScript, sh, ASP, Verilog, JavaScript, Scheme, Rust, Nim, INTERCAL, sed, Isabelle, Visual Basic, zsh, AlokScript, Coq, Idris, Hack, Prolog, Whitespace, PureScript, Go, Odin, Haskell, Python, tcsh, Unison, Clingo, Bash, Java, Zig, Cyclone, PHP, awk, C, ActionScript, C++.
But Lean is the best.
Why?
Because it's perfectable. It's not perfect, but it is perfectable. You can write down properties about Lean, in Lean.
The whole edifice of these facts and properties shall be known as progress.
In every language, you eventually wanna say stuff about the code itself.
Like here's a function that always returns 5, but in almost no language can you really use that fact in a way that the language itself helps you with.
function returnFive(x : number) : number {
return 5;
}
def returnFive (unused variable `x`
Note: This linter can be disabled with `set_option linter.unusedVariables false`x : Int) : Int := 5
theorem returnFive_eq_five (x : Int) : returnFive x = 5 := rfl
example (a : Int) : 6 = returnFive a + 1 := bya:Int⊢ 6 = returnFive a + 1
unfold returnFivea:Int⊢ 6 = 5 + 1
rflAll goals completed! 🐙
Languages without types tend to grow them, like PHP in 7.4 and Python type annotations, and the general trend towards TypeScript and Rust.
Inevitably, people want to push types. Even Go. C++ templates are the ultimate
example. If it can be computed at compile time, at some point someone wants
to, like Rust's ongoing constification.
But the easiest way to do anything is properly. Doing it properly is basically dependent types. There are fancier things than them, but like Turing-completeness, dependent types can get you there. Hence perfectable.
On top of the types, you want infrastructure for showing 2 types are equal/not equal. This is basically a theorem prover. Any dependent language can become a theorem prover, but it needs to grow the nice API we call "theorem proving infrastructure".
That's half the story. The semantics half. The syntax half is metaprogramming and custom syntax.
Metaprogramming
Most languages have no facility for this, or it's a bit awkward, like Rust's procedural macros.
Lean is freakishly seamless. Here's tic-tac-toe with a custom board notation:
/-- The two players in tic-tac-toe. -/
inductive Player where
| X
| O
deriving BEq, Inhabited
/-- A square on the board: either empty or occupied by a player. -/
inductive Square where
/-- Nobody has played here yet. -/
| empty
/-- A player has claimed this square. -/
| occupied (player : Player)
deriving BEq, Inhabited
@[simp] def boardSize : Nat := 9
/-- A 3x3 tic-tac-toe board. -/
structure Board where
squares : Array Square
deriving BEq
Now the custom syntax:
/-- A cell in the board literal: `X`, `O`, or `_` (empty). -/
declare_syntax_cat tttCell
syntax "X" : tttCell
syntax "O" : tttCell
syntax "_" : tttCell
/-- A row of three cells separated by `|`. -/
declare_syntax_cat tttRow
syntax (name := tttRowRule) tttCell "|" tttCell "|" tttCell : tttRow
/-- Three rows make a complete 3x3 board. -/
declare_syntax_cat tttBoardSyntax
syntax tttRow tttRow tttRow : tttBoardSyntax
/-- Elaborate a single cell into a `Square`. -/
private def elabTttCell (stx : Lean.Syntax) : Lean.Elab.Term.TermElabM Square :=
match stx with
| `(tttCell| X) => pure (.occupied .X)
| `(tttCell| O) => pure (.occupied .O)
| `(tttCell| _) => pure .empty
| _ => Lean.throwError s!"unsupported cell syntax {stx}"
open Lean Elab Term in
/-- `board!` turns a visual board layout into a `Board` at compile time.
Each cell is validated during elaboration. -/
elab "board! " b:tttBoardSyntax : term => do
let mut squares : Array Square := #[]
unless b.raw.getNumArgs = 3 do
Lean.throwError s!"Expected 3 rows, got {b.raw.getNumArgs}"
for rowIdx in [:3] do
let row := b.raw.getArg rowIdx
unless row.isOfKind `tttRowRule do
Lean.throwError s!"malformed tttRow"
let cells := #[row.getArg 0, row.getArg 2, row.getArg 4]
for cell in cells do
squares := squares.push (← elabTttCell cell)
unless squares.size = boardSize do
Lean.throwError s!"internal error: expected 9 squares, got {squares.size}"
let squareTerms ← squares.mapM fun sq =>
match sq with
| .empty => `(Square.empty)
| .occupied .X => `(Square.occupied Player.X)
| .occupied .O => `(Square.occupied Player.O)
let arrSyntax ← `(#[$squareTerms,*])
let boardTerm ← `(Board.mk $arrSyntax)
Lean.Elab.Term.elabTerm boardTerm none
X | O | _
_ | X | _
O | _ | X#eval board!
X | O | _
_ | X | _
O | _ | X
Win X#eval getGameStatus (board!
X | X | X
O | O | _
_ | _ | _)
X | O | _
_ | X | _
O | _ | XWin X
This lets you design APIs in layers and hide them behind syntax. Plus the
interpretation of the syntax can be swapped easily. Lean's type system helps a
bit with the metaprogramming (but I would love to see meta-metaprogramming with
some sort of modality for better infra around Lean Syntax).
def «🎮 tic tac toe 🎮» : Board := board!
X | O | X
O | X | O
X | _ | O
Win X#eval getGameStatus «🎮 tic tac toe 🎮»
Win XDoing this properly just is a theorem prover. Theorem proving comes about from convergent evolution in programming.
Speed
This is the biggest one. Slow languages suck. Why use a computer then.
Lean could be faster. It's not Rust-fast, but it has a very high ceiling for optimization thanks to the ability to show 2 pieces of code equal.
/-- If two functions are provably equal on all inputs,
the compiler can freely substitute one for the other. -/
theorem five_plus_one_eq_six : ∀ a : Int, returnFive a + 1 = 6 := by⊢ ∀ (a : Int), returnFive a + 1 = 6
intro aa:Int⊢ returnFive a + 1 = 6
unfold returnFivea:Int⊢ 5 + 1 = 6
rflAll goals completed! 🐙
Leo de Moura seems convinced of the need for this too, enough that backward compat is going by the wayside. Thankfully in AI world rewriting code is a lot easier, and a theorem prover is the ultimate refactoring tool (how could it not be?)
Community
Lean is the only language in its class that's actually gaining traction. Coq, Idris, Agda — none of them are really competing anymore. Idris would otherwise count as a real programming language that's also a prover, but the community never reached critical mass. F* could count too, but its community is a rounding error. Lean is the one with raw programming ability that's also a theorem prover, and it's growing.
the Lisp curse
Powerful metaprogramming usually comes with a curse. The Lisp curse: it's so easy to roll your own that nobody ever finishes anything. Mark Tarver's classic line was about Lisp GUIs — 9 offerings, none documented, none bug-free, each person happy with their own. Tragedy of the commons.
The C/C++ approach is the opposite. It's so damn hard to do anything with tweezers and glue that anything significant is a real achievement. You want to document it. You need help, so you get social. You work with others just to get somewhere.
Formalizing math is "so damn hard" in exactly the same way, and it's united the community. mathlib is the cathedral. Smaller projects are the bazaar, and the bazaar upstreams finished work back to mathlib. This isn't a theoretical claim — it already happened.
Whether Lean escapes the curse on the software side too is less clear. But the mathematician userbase has so far also rallied around shared software needs: Lake, Elan, Reservoir, one dominant standard library. The language has Terence Tao, Peter Scholze, and Leo de Moura as leadership to turn to. That's enough gravity to keep people pulling the same direction.
This blog post is itself Lean code.