A Perfectable Programming Language

a perfectable programming language

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 (x : Int) : Int := 5
theorem returnFive_eq_five (x : Int) : returnFive x = 5 := rfl
example (a : Int) : 6 = returnFive a + 1 := a:Int⊢ 6 = returnFive a + 1
a:Int⊢ 6 = 5 + 1
All 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 const ification.

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:

inductive Player where | X | O
inductive Square where | empty | occupied (player : Player)

declare_syntax_cat tttCell
syntax "X" : tttCell
syntax "O" : tttCell
syntax "_" : tttCell

elab "board! " b:tttBoardSyntax : term => do
  -- ... logic to transform syntax into a Board structure

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.

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.

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.

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. Lean is the one with raw programming ability that's also a theorem prover, and it's growing.