Program = Proof

This course provides a first introduction to the Curry-Howard correspondence between programs and proofs, from a theoretical programmer's perspective: we want to understand the theory behind logic and programming languages, but also to write concrete programs (in OCaml) and proofs (in Agda). After an introduction to functional programming languages, we present propositional logic, λ-calculus, the Curry-Howard correspondence, first-order logic, Agda, dependent types and homotopy type theory.

What Hacker News says

leonidasrupAug 2026

I would highly recommend "PROGRAM = PROOF" by Samuel Mimram.

It covers everything from pure lambda calculus through dependent type theory up to homotopy type theory. In comparison to the HoTT book, the book "PROGRAM = PROOF" is oriented less towards mathematicians more towards programmers. It contains also a short introduction to OCaml and Agda.

The book can downloaded from the authors web page:

https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching...

https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/publicat...

thread

boxfireMay 2025

There's a book that's explicitly about this, "Program = Proof", and though it's not beginner and needs maybe a light version for earlier learners, is an excellent example.

thread

nextosOct 2023

Formal Methods An Appetizer is excellent and has a companion site with toy formal methods implemented in F#: http://www.formalmethods.dk. However, it does not cover proof assistants.

Alternatively you may enjoy these two. The latter is especially thorough, and begins with classical logic:

* Concrete Semantics (Isabelle): http://concrete-semantics.org

* Program = Proof (Agda): https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching...

thread

comonoidAug 2023

1. Program = Proof by Samuel Mimram

Math foundation of programming. Church–Rosser theorem, Curry–Howard correspondence, intuitionistic logic, theorem proving with dependent types, etc.

2. Rust Atomics and Locks: Low-Level Concurrency in Practice by Mara Bos

Great introduction even for non-Rust programmers.

3. Statistical Consequences of Fat Tails by N. Taleb et al.

I've just started to read it, but looks promising (lot of mathematical statistics).

thread

nextosJul 2023

Program = Proof, Samuel Mimram: https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching.... Also available as hardcopy in Amazon.

thread

nextosJan 2023

These are good recommendations, but I think beginners tend to burn out due to the lack of a structured program and/or exercise solutions if they are trying to study on their own. The simplest structured program I can think of that satisfies both is:

* Basic Mathematics by Lang. Covers basic algebra and geometry at high school level.

Then one of these two, depending on your interests, or both:

* Vector Calculus, Linear Algebra and Differential Forms by Hubbard and Hubbard. Takes you through linear algebra, single-variable calculus and multiple variable calculus. Analysis is discussed in an appendix. All proofs have a constructive bias, so it's very algorithmic and natural for a CS-minded student. Solutions are in a separate volume.

* Program = Proof by Mimram. Discusses logic and computation, and takes you from the basics to depedent type theory and beyond. Uses OCaml and Agda. Freely available at: https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching...

thread