## Specification in Lean

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 Lean, and is packaged as mathlib4. A good introduction to the use of Lean for the formalisation of mathematics is Theorem Proving in Lean.

The programming language component of Lean (version 4) is a comprehensive functional programming language, in the style of Haskell. A good introduction to the use of Lean as a programming language is Functional Programming in Lean. 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 verify or 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**).

### Creating The Markdown Files

The files are Lean scripts from which markdown is generated using the mdgen tool.

Build the markdown files with `lake exe mdgen LeanSpec md`

.

### Acknowledgement

Thanks to Kevin Buzzard, Mario Caneiro and Partick Massot for their valuable comments.