Lean is a dependently typed functional programming language that incorporates the correspondence between propositions and types (and between proofs and programs). As such it is able to serve as a basis for the formalisation of mathematics (i.e., the statement and proof of theorems). Indeed, a considerable body of mathematics has been formalised in version 3 of Lean, and is packaged as mathlib. A good introduction to the use of Lean for the formalisation of mathematics is Theorem Proving in Lean.
The programming language component of Lean 3 primarily serves as the meta-language for performing proofs. At the time of writing Lean 4 is in an advanced stage of development. In addition to maintaining the capabilities of Lean 3 concerning formalisation of mathematics, significant effort has gone into developing Lean 4 (hereafter simply referred to as Lean) as a comprehensive functional programming language, in the style of Haskell.
While Haskell has a more traditional type system, the dependently typed system of Lean and its underlying logic bring a number of benefits from a software perspective:
- Lean is a fully featured specification language. It can be used to specify the functionality of software that can be implemented in Lean or other languages.
- Lean software can be verified in Lean itself (using the same logic employed for mathematical proof).
- When a Lean specification is viewed as a theorem in the Lean logic, a proof of that theorem yields a program that satisfies the specification.
The cost of this capability is that the type system is undecidable: the system cannot, given a program and a type (specification), determine automatically whether the program meets the specification. A proof is required. When the dependent type theory of Lean is used to its full capacity, type correctness = program correctness.
This tutorial is an introduction to the use of Lean for the specification of software functionality. The aim is to express what a function is intended to achieve, not how it is achieved. How one might derive a program that meets a specification using the Lean logic is not addressed here. The contents of this tutorial are:
| Introduction | Introduction to Lean as a specification language |
| Quotient & Remainder | Quotient and remainder on division |
| Sort | Sorting a list of items |
| Knapsack | Knapsack: an optimisation problem |
| Graph | Graph searching |
| TMI | A scheduling example from the aviation industry |
| Flight Planning | Flight planning message processing example from the aviation industry |
The following supplementary modules support the example specifications:
| Util | General purpose functions that could in future appear in a standard library |
| Temporal | A simple theory of dates, times, durations and intervals |
| Geo | Basic geospatial entities |
Some discussion on the use of Lean for specifications is here (to do).
The files are Lean scripts from which markdown is generated. Python and the lean2md package are required. To build and serve the markdown files locally, Rust and mdbook are required.
Build the markdown files with lake run md.
Build the book and serve with mdbook serve.
Thanks to Kevin Buzzard, Mario Caneiro and Partick Massot for their valuable comments.