This is not about Lean Kanban, which I hear about at work with increasing frequency, but about Lean, Microsoft Research's extraordinarily wonderful dependently typed language and formal verification system. In this series of posts, I want to put a few things in order in my own head, create a simple reference, and help people appreciate the system if, for some unfathomable reason, they cannot be bothered to read the book—even though they absolutely should. It is, in truth, close to the ideal of how books of this kind ought to be written. The book leads the reader through the intricacies of formal verification with a dependently typed system almost under anaesthesia. So of course you would be better off closing this post and reading it instead. But I am writing this for myself, after all!
This article sat in my drafts for more than a year. When I opened it today, I realised that it was actually 90% complete. So I decided to finish just a couple of paragraphs and finally publish it, leaving all the most interesting material for future instalments—which, at my publication rate, will presumably appear in another two years.
Before looking at Lean itself, we need to understand what problem we are solving and why it needs solving at all. Let us begin by introducing the notion of formal verification, already mentioned twice above. By this we mean the use of logical and computational methods to establish the truth of statements expressed as precise mathematical formulas. One example is the following simple expression, which we will certainly prove formally one day:
Such expressions may describe not only classical mathematical theorems, as in the example above, but also statements about the correctness of program code, hardware circuits, network protocols, and much else. This breadth is made possible by the Curry–Howard correspondence, which says that checking the correctness of a theorem's proof and checking whether a function satisfies its declared specification—that is, its type—are essentially the same thing. Proof does not come for free, of course. First, any system whose correctness is to be verified must be formalised in mathematical terms, which can be far from trivial. Second, correctness checking itself is often computationally difficult and consumes substantial hardware resources.
Wait—what is all this for?
Well, first of all, it is beautiful. More seriously, I see two main motivations for formal verification and automated proving—that is, synthesising part of a proof without human involvement.
The first, fundamental motivation is finally to teach machines to reason logically and derive new knowledge from what they already know. All our fashionable neural networks are excellent at generalisation and pattern recognition, but dreadful at drawing logical conclusions from data. It is a joy to watch the hyped-up GPT-3 fail at the simplest questions. Only a synthesis of these disciplines may one day lead us to genuine artificial general intelligence.
The second, practical motivation is to be certain that theorem proofs contain no errors. Modern proofs are extremely complex and run to hundreds of pages—here, for example, is a 109-page proof of Fermat's Last Theorem—so checking them is no easier than writing them in the first place. How can we be sure that a hundred-page proof contains no mistake? Until now, there has been only one method: give it to several authoritative mathematicians and believe their verdict. Imagine that: mathematics, queen of the sciences, reduced to faith in authority! The very notion of a “true statement” loses its mathematical purity because it may turn out to be false tomorrow. How are we supposed to look down on the experimental sciences now? Let a machine check the proof!
There are also people who sincerely believe that these methods will enable us to produce higher-quality software, but lately I have become rather sceptical. Why do I not believe it? Although this series will argue that all this magic is simple and comprehensible, applying such approaches to software development is in fact very difficult. A formal proof takes far more work than the equivalent tests, while the difference between 100% and 99% system reliability is not that critical. There are very few fields willing to pay a premium for that final percentage, so the area will remain a niche pursuit.
A few words about types
I will not describe CoC (the Calculus of Constructions) or CiC (the Calculus of Inductive Constructions), on which all modern dependently typed languages used for proofs are built, in any detail. But a few basic introductory remarks are worthwhile.
Types can be regarded as an alternative to sets, which long served as the “basic language” of mathematics. In other words, starting from the simplest set-theoretic axioms—studied extensively in schools and in the early years of technical universities—we can reach arbitrary mathematical constructions, from natural numbers to multidimensional geometric objects. Unfortunately, despite its axiomatic simplicity and descriptive power, set theory itself has a fundamental flaw: it is inconsistent, which means that, if one wishes, its tools can be used to prove anything, including obviously false statements.
Another feature widely used in school mathematics that is worth abandoning is the non-constructive nature of proofs: proving a fact does not necessarily give you the object whose existence is being proved. For example, suppose you prove that there are two irrational numbers, and , such that is rational, but do not produce the numbers themselves. What use is a proof like that?
This gave rise to two movements of great importance to our subject: type theory and intuitionism.
Type theory—more precisely, the version we will consider here—imposes a strict hierarchy on the membership of objects, or terms, in collections called types. Every primitive object belongs to one set or another: a type of order zero. These types form a universe called Type 0, but the sets themselves cannot belong to other sets. Instead, they belong to larger structures: types of order one, or Type 1. Continuing in the same way gives us the rule that every type of order u belongs to a type of order u+1: Type u : Type (u+1). This avoids paradoxes by making the description of the constructions still more rigorous. The final ingredient is the cumulative nesting of type universes. This means that a type belongs not only to the type one level above it, but to every universe of a higher order.
At its simplest, by intuitionism we mean the absence of the law of excluded middle (A ∨ ¬A), or equivalently of double-negation elimination (¬¬A → A). Philosophically, this means that refuting a fact does not constitute a proof of its negation. In other words, the only way to prove something in intuitionism is to provide a construction—the constructive method of proof. To prove that there are natural numbers below 10, for example, one must produce at least one such number. To prove the commutativity of natural-number addition mentioned above, one must show a way to reduce both sides to the same result. We will make extensive use of this idea, producing concrete examples of terms whose types contain the propositions we want to prove.
Setup
Lean 3 can be downloaded from GitHub or from your operating system's repositories. While this text was being prepared, the 3.x branch was frozen—although it continues as a community branch. Version 4 is now under active development but is still extremely unfriendly to users.
To use the language properly, we need a compatible IDE. At present, the options include Emacs, VIM, and VS Code. I use the last of these, where the whole process looks like this:
The language makes extensive use of Unicode, which you can enter directly. To obtain the attractive ℕ symbol in VS Code, simply type \nat; the equally attractive lambda (λ) is entered with \fun or \lam. The main disadvantage of using Lean in VIM is probably its lack of proper support for this feature. In other respects, it is no less convenient:
Hello World
Lean was designed primarily for formal verification, not programming in the conventional sense. Nevertheless, we can easily print any string using the #print command. To do so, create the simplest possible file—say, hello_world.lean:
#print "Hello World!"
Then run it from the command line as follows:
lean hello_world.lean
Hello, World!From this point onward we will not launch Lean from the command line, preferring to work in an interactive environment. You could write Lean in Notepad, however: every command beginning with # prints information to stdout when processed by the Lean interpreter.
Type inference
The basic command we will use constantly is #check, which checks the type of an expression. Here are several examples:
#check 5
#check 'a'
#check tt
During evaluation, each line returns the type of its expression:
5 : ℕ
'a' : char
tt : bool
In Lean, not only primitive values but also functions and types are first-class objects. They can be used as function arguments and return values, so they too must have types:
#check ℕ
#check fun x, x + 1
These return, respectively:
ℕ : Type
λ (x : ℕ), x + 1 : ℕ → ℕ
An arrow expression can also be typed—to enter the attractive arrow, use the \r abbreviation:
#check ℕ → ℕ
As expected, this expression again returns Type.
The Type expression itself can be typed, because it is a type and, as we have already said, types in Lean are first-class objects.
#check Type
Because Lean is a language based on the calculus of predicative inductive constructions, all types form a cumulative hierarchy. Type (0) belongs to Type 1 and every higher universe, Type n. Our query displays the nearest one:
Type : Type 1
The standard library also defines product and sum types, both useful things to have around. They have appropriately descriptive names as well as attractive Unicode notation:
#check prod ℕ ℕ
#check ℕ × ℕ
#check (1, 1) -- has type ℕ × ℕ
prod can be replaced by the × operator (\x)
#check sum nat bool
#check nat ⊕ bool
sum can be replaced by the ⊕ operator (\o+)
Evaluation and reduction
As in any respectable programming language, we can ask Lean to evaluate an expression. The #eval command is used for this:
#eval 1 + 2 -- 3
#eval (λ x, x + 39) 3 -- 42
#eval tt && ff -- ff
Lean can be used as a calculator
Not every computation, however, ends with a result that can be represented as an elementary machine type. The more general construct is therefore #reduce, which produces the result in normal form:
#reduce (λ x y, x) 1 -- λ (y : ?M_1), 1
This output also shows how a type can be specified in a lambda abstraction—that is, how to use Church style. We can put that to use in the following example:
#reduce (λ (x : ℕ) (y : ℕ), x + 10) 1 4 -- 11
In principle, #reduce can always be used instead of #eval. The latter performs better, but until we start using Lean for general-purpose programming, consistency is more important than the difference in convenience.
Functions
Writing nothing but lambdas would obviously be rather inconvenient, so Lean provides a mechanism for binding names to terms. Here, for example, we define a constant, or nullary, function named foo that returns the natural number 5:
def foo : ℕ := 5
A less trivial example binds a name to a type, which in Lean is no different from any other term:
def my_bool : Type := bool
It is time to move from constant functions to more interesting functions with parameters. They can be defined in several equivalent ways, depending entirely on the user's habits and aesthetic sensibilities. This is possible because all Lean functions are curried by default, as in Haskell.
def add1 (n : ℕ) (m : ℕ) : ℕ :=
n + m
def add2 (n m : ℕ) : ℕ :=
n + m
def add3 (n : ℕ) : ℕ → ℕ :=
λ m, n + m
def add4 : ℕ → ℕ → ℕ :=
λ n m, n + m
Support for dependent types allows arguments to appear in a function's return type. This means that in the arrow A → B, the type B depends on the value a; in other words, a somehow appears in the expression for B. This construct is conventionally written Π (a : A), B. The arrow above is syntactic sugar for the special case in which B does not depend on a. Nevertheless, we can write a fully desugared version:
def add5 : Π (n : ℕ), Π (m : ℕ), ℕ :=
λ n m, n + m
In the simplest case, A → B and Π (a : A), B are the same thing
Like any respectable language, Lean supports fairly advanced argument pattern matching. This allows us to combine everything we have learned and apply it to something of great practical value: a Fibonacci-number function, for example.
def fib : ℕ → ℕ
| 0 := 1
| 1 := 1
| (n + 2) := fib n + fib (n + 1)
#eval fib 10 cheerfully prints 89
That is it—we can program now! But that is not, of course, why we are here. Next time, we will introduce several constructs unusual in conventional programming languages, examine implementations of different type systems, and finally plunge into theorems.