1.2.1. Logic🔗

Logic is the field of study whose subject matter is proofs -- unassailable arguments for the truth of particular propositions. Volumes have been written about the central role of logic in computer science. Manna and Waldinger (1971)Zohar Manna and Richard J Waldinger (1971). “Toward automatic program synthesis”. Communications of the ACM. 14(3). called it "the calculus of computer science," while Halpern et al. (2001)Joseph Y Halpern, Robert Harper, Neil Immerman, Phokion G Kolaitis, Moshe Y Vardi, and Victor Vianu (2001). “On the unusual effectiveness of logic in computer science”. Bulletin of Symbolic Logic. 7(2).'s paper On the Unusual Effectiveness of Logic in Computer Science catalogs scores of ways in which logic offers critical tools and insights. Indeed, they observe that, "As a matter of fact, logic has turned out to be significantly more effective in computer science than it has been in mathematics. This is quite remarkable, especially since much of the impetus for the development of logic during the past one hundred years came from mathematics."

In particular, the fundamental tools of inductive proof are ubiquitous across computer science. You have surely seen them before, perhaps in a course on discrete math or analysis of algorithms, but in this book we will examine them more deeply than you have probably done so far.

1.2.2. Proof Assistants🔗

The flow of ideas between logic and computer science over the years has run in both directions, with CS also making key contributions to logic. One of these has been the development of software tools for helping construct and validate proofs of logical statements. These tools fall into two broad categories:

• Automated theorem provers provide "push-button" operation: you give them a proposition and they return either true or false (or, sometimes, don't know: ran out of time). Although their reasoning capabilities are limited, they have matured tremendously in recent decades and are used now in a multitude of settings. Examples of such tools include SAT solvers, SMT solvers, and model checkers.

• Proof assistants — or just provers — are hybrid tools that automate the more routine aspects of creating proofs while depending on human guidance for more difficult aspects. Widely used proof assistants include Isabelle, Agda, Twelf, ACL2, PVS, F*, HOL4, Rocq, and Lean, among many others.

This course is based around Lean, a prover that has been under development since 2013 and that has attracted a large and active community of users in both research and at companies like DeepMind, OpenAI, Anthropic, MSR, and AWS.

Lean provides a rich environment for interactive development of machine-checked formal reasoning. The kernel of the Lean system is a simple proof-checker, which guarantees that only correct deduction steps are ever performed. On top of this kernel, the Lean environment provides high-level facilities for proof development, including a large library of common definitions and lemmas, powerful tactics for constructing complex proofs semi-automatically, and a highly extensible system for defining new proof-automation tactics and notations for specific situations.

Lean and its relatives have become critical enablers for a huge variety of work across computer science and mathematics:

• As a platform for modeling programming languages, proof assistants have become standard tools for researchers who need to describe and reason about complex language definitions. They have been used, for example, to check the security of the JavaCard platform, obtaining the highest level of common criteria certification, and for formal specifications of the x86 and LLVM instruction sets and programming languages such as C.

• As environments for developing formally certified software and hardware, they have been used, for example, to build CompCert (Leroy et al., 2016)Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus Pister, and Christian Ferdinand, 2016. “CompCert - A Formally Verified Optimizing Compiler”. In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress., a fully-verified optimizing compiler for C, Cedar (Disselkoen et al., 2024)Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks, Kesha Hietala, John Kaster, Anwar Mamat, Matt McCutchen, Neha Rungta, and others, 2024. “How We Built Cedar: A Verification-Guided Approach”. In Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering., a formally-specified policy language, and CertiKOS (Gu et al., 2016)Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Newman Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo, 2016. “CertiKOS: An extensible architecture for building certified concurrent OS kernels”. In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16)., a fully verified hypervisor, and for proving the correctness of subtle algorithms involving floating point numbers, and as the basis for CertiCrypt, FCF, and SSProve, which are frameworks for proving cryptographic algorithms secure. They are also being used to build verified implementations of the open-source RISC-V processor architecture.

• As proof assistants for mathematics, they have been used to validate and help develop a number of important results. For example, the ability to include complex computations inside proofs made it possible to develop the first formally verified proof of the 4-color theorem, which had previously been controversial among mathematicians because the argument required checking a large number of configurations using a program. More recently, an even more massive effort led to a formalization of the Feit-Thompson Theorem, the first major step in the classification of finite simple groups.

  Lean, in particular, is now at the core of various formalization efforts in mathematics, such as the proof of Fermat's Last Theorem, the Sphere Packing Problem. and even DeepMind's AI model for International Math Olympiad problems, AlphaProof.

1.2.3. Functional Programming🔗

Functional programming refers both to a collection of powerful coding idioms that can be used in almost any programming language and to a family of languages designed to foreground these idioms, including Haskell, OCaml, Standard ML, F#, Scala, Scheme, Racket, Common Lisp, Clojure, Erlang, F*, and Lean itself.

Functional programming has been developed over many decades — indeed, its roots go back to Church's lambda-calculus from the 1930s, well before the first electronic computers! But since the early '90s it has enjoyed a surge of interest among both software engineers and language designers.

The basic tenet of functional programming is that, whenever possible, computation should be pure, in the sense that the only effect of execution should be to produce a result. That is, it should be free from side effects such as I/O, assignments to mutable variables, redirecting pointers, etc. For example, whereas an imperative sorting function might take a list of numbers and rearrange its pointers to put the list in order, a pure sorting function would take the original list and return a fresh list containing the same numbers in sorted order.

A significant benefit of this style of programming is that it makes programs easier to understand and reason about. If every operation on a data structure yields a new data structure and leaves the old one intact, then there is no need to worry about how that structure is being shared and whether a change by one part of the program might break an invariant relied on by another part of the program. This is particularly important when reasoning about concurrent systems, where every piece of mutable state shared between threads is a potential source of pernicious bugs.

Another reason for the popularity of functional programming, related to the first, is that functional programs are often much easier to parallelize and physically distribute than their imperative counterparts. If running a computation has no effect other than producing a result, then it does not matter where it is run. Likewise, if a data structure is never modified destructively, it can be copied freely, across cores or across the network. Indeed, the "Map-Reduce" idiom, which lies at the heart of massively distributed query processors like Hadoop and is used by Google to index the entire web, is a classic example of functional programming.

For these books, functional programming has yet another significant attraction: it serves as a bridge between logic and computer science. Indeed, Lean itself can be viewed as a combination of a small but extremely expressive functional programming language and a set of tools for stating and proving logical assertions. Moreover, when we come to look more closely, we find that these two sides of Lean are actually aspects of the very same underlying machinery -- i.e., proofs are programs.

1.2.4. Further Reading🔗

This text is intended to be self contained, but readers looking for follow-on textbooks or deeper treatments of particular topics will find some suggestions for further reading in the Postscript chapter.

1.3.1. System Requirements🔗

Lean runs on Linux, MacOS, and Windows. The files in this book have been tested with Lean version 4.34.0-rc2.

1.3.2. Installation🔗

The Visual Studio Code IDE is the recommended platform for using Lean. To get set up, follow these steps:

• Install VS Code if needed.

• From the Extensions tab of VS Code, install the Lean 4 extension.

• Download the book, build it if necessary — more below.

• Open the built book directory in a VS Code window.

• Open a Lean file; the extension will offer to install Lean; accept, and it will fetch the version this book needs.

• Wait for Lean to build the project (it takes a few minutes).

code _out/lf/student/lean

cd _out/lf/student/lean
code .

python3 -m http.server 8000 -d _out/lf/student/html

1.3.3. Exercises🔗

Each chapter includes numerous exercises. Each is marked with a "star rating," which can be interpreted as follows:

• One star: easy exercises that underscore points in the text and that, for most readers, should take only a minute or two. Get in the habit of working these as you reach them.

• Two stars: straightforward exercises (five or ten minutes).

• Three stars: exercises requiring a bit of thought (ten minutes to half an hour).

• Four and five stars: more difficult exercises (half an hour and up).

Those using SF in a classroom setting should note that the autograder assigns extra points to harder exercises:

1 star  = 1 point
2 stars = 2 points
3 stars = 3 points
4 stars = 6 points
5 stars = 10 points

Some exercises are marked "advanced," and some are marked "optional." Optional exercises provide a bit of extra practice with key concepts and introduce secondary themes that may be of interest to some readers. Advanced exercises offer an extra challenge and a deeper cut at the ideas. Doing just the non-optional, non-advanced exercises should provide good coverage of the core material.

1.3.4. Citation Format🔗

If you want to refer to this volume in your own writing, please do so as follows:

@book            {SFL:1,
author       =   {Mike Hicks and Benjamin C. Pierce and the SF-in-Lean team},
title        =   "Logical Foundations",
series       =   "Software Foundations in Lean",
volume       =   "1",
year         =   "2026",
publisher    =   "Electronic textbook",
note         =   {Version 0.1.0, \URL<https://github.com/plclub/sf-in-lean>}
}

1.5.1. Credits🔗

Leadership: Mike Hicks and Benjamin C. Pierce lead the SF-in-Lean project.

Authors: The Lean adaptation of Software Foundations was created by Mike Hicks, Benjamin C. Pierce, One An, Roger Burtonpatel, Jonathan Chan, Harry Goldstein, Niklas Halonen, Chris Henson, Kihong Heo, Yipeng Liu, and Daniel Sainati

... with contributions from Luisa Cicolini, Michael Clarkson, Robert Joseph, Sati, and Shriya Thakur

... and gratitude to David Thrane Christiansen, for helping us understand the intricacies of Lean's Verso document preparation system.

SF in Rocq: The first three volumes of Software Foundations in Lean (Logical Foundations in Lean, Type Systems in Lean, and Hoare Logic in Lean) are adapted from the Logical Foundations and Programming Language Foundations volumes of the original Software Foundations series in Roqc, developed from 2008 to 2026 by a team of authors and contributors led by Benjamin C. Pierce.

The original Logical Foundations was written by Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cătălin Hriţcu, Vilhelm Sjöberg, and Brent Yorgey, with contributions from Loris D'Antoni, Andrew W. Appel, Arthur Charguéraud, Michael Clarkson, Anthony Cowley, Jeffrey Foster, Dmitri Garbuzov, Olek Gierczak, Michael Hicks, Ranjit Jhala, Ori Lahav, Yishuai Li, Greg Morrisett, Jennifer Paykin, Mukund Raghothaman, Chung-chieh Shan, Leonid Spesivtsev, Caleb Stanford, Andrew Tolmach, Philip Wadler, Stephanie Weirich, Li-Yao Xia, and Steve Zdancewic.

The original Programming Language Foundations was written by Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cătălin Hriţcu, Vilhelm Sjöberg, Andrew Tolmach, and Brent Yorgey with contributions from Loris D'Antoni, Andrew W. Appel, Arthur Chargueraud, Michael Clarkson, Anthony Cowley, Jeffrey Foster, Dmitri Garbuzov, Michael Hicks, Ranjit Jhala, Ori Lahav, Yishuai Li, Greg Morrisett, Jennifer Paykin, Mukund Raghothaman, Chung-Chieh Shan, Leonid Spesivtsev, Caleb Stanford, Philip Wadler, Stephanie Weirich, Li-Yao Xia, and Steve Zdancewic.

Funding: Development of the original Software Foundations series was supported, in part, by the National Science Foundation under the NSF Expeditions grant 1521523, The Science of Deep Specification.