12.1. Looking Back🔗

We've covered quite a bit of ground. Along the way, we developed three connected themes:

Functional programming:

• recursive definitions over immutable data

• higher-order functions

• polymorphism

Logic, the mathematical basis for software engineering:

       logic                        calculus
--------------------   ~   ----------------------------
software engineering       mechanical/civil engineering

• inductively defined propositions and relations

• inductive proofs

• proof objects

Lean, an industrial-strength proof assistant:

• a functional programming language

• tactics for constructing proofs

• proof automation

12.2. Looking Forward🔗

The next volumes carry these ideas into programming-language theory and program verification:

• Type Systems develops operational semantics and type systems, including the simply typed lambda calculus and the progress and preservation theorems.

• Hoare Logic introduces imperative programs and Hoare logic, a framework for stating and proving correctness properties of programs with mutable state.

Both volumes build directly on the definitions and proof techniques introduced here.

12.3. Resources🔗

This volume also contains optional sections and exercises that develop some topics further.

For questions about Lean, the Lean community Zulip is an active place to ask questions and discuss formalization.

The following books continue in several different directions:

• Functional Programming in Lean explores Lean as a programming language.

• Theorem Proving in Lean 4 gives a systematic introduction to Lean's logic and proof language.

• Mathematics in Lean develops formalized mathematics using Lean and Mathlib.