Type Theory and Formal Proof

What Hacker News says

1. LightMachineSep 2026
   There isn't a single book that covers all of it... Bend's theory touches various domains (dependent types, substructural types, termination). And then there's the runtime, compiler, GPU kernels...

   If you mean about the type theory specifically, "Type Theory and Formal Proof by Nederpelt and Geuvers" is a good introduction. Not sure what I'd recommend on linear types, no book I know of is very introductory? Perhaps "Idris 2: Quantitative Type Theory in Practice", which is a language with similar foundations to Bend, and the author wrote a book on it (and inspired myself!)

   Show morethread
2. roadside_picnicJan 2026
   > It is still likely very tedious to confirm what the LLMs say,

   A large amount of Tao's work is around using AI to assist in creating Lean proofs.

   I'm generally on the more skeptical side of things regarding LLMs and grand visions, but assisting in the creation of Lean proofs is a huge area of opportunity for LLMs and really could change mathematics in fundamental ways.

   One naive belief many people have is that proofs should be "intelligible" but it's increasingly clear this is not the case. We have proofs that are gigabytes (I believe even terabytes in some cases) in size, but we know they are correct because they check in Lean.

   This particular pattern of using state of the art work in two different areas (LLMs and theorem proving) absolutely has the potentially to fundamentally change how mathematics is done. There's a great picture on pp 381 of Type Theory and Formal Proof where you can easily see how LLMs can be placed in two of the most tricky parts of that diagram to solve.

   Because the work is formally verified we can throw out entire classes of LLM problems (like hallucinations).

   Personally I think strongly typed language, with powerful type systems are also the long term ideal coding with LLMs (but I'm less optimistic about devs following this path).

   Show morethread
3. griffzhowlSep 2025
   I've got interested in formalization of mathematics recently and found the book Type Theory and Formal Proof by Nederpelt and Geuvers is a really nice one, taking you from the untyped lambda calculus and gradually extending the type system until you get the full dependent type theory and the Calculus of Constructions that underlies, e.g., the Lean language/proofchecker

   Peter Smith (logic God) also recommends it in his logic study guide:

   https://www.logicmatters.net/tyl/

   Show morethread
4. codeismathAug 2025
   Books. Some books on my shelf covering these topics:

   "Type Theory and Functional Programming" by Simon Thompson (PDF available via quick search)

   First 120 pages of "Type Theory and Formal Proof" by Rob Nederpelt / Herman Geuvers

   For some early stuff on dependent types (also covered in the above), check out "Intuitionistic Type Theory" by Per Martin-Lof

   "Computation and Reasoning: A Type Theory for Computer Science" by Zhaouhui Luo

   "Type-Driven Development with Idris" by Edwin Brady

   "Gentle Introduction to Dependent Types with Idris" by Boro Sitnikovski

   "Types and Programming Languages" by Pierce

   "Practical Foundations for Programming Languages" by Robert Harper (or any of his YouTube videos re/Type Theory)

   "The Little Typer" by Friedman and Christiansen

   "Modal Homotopy Type Theory: The Prospect of a New Logic for Philosophy" by David Corfield (just took this one to OBX North Carolina to enjoy on my beach vacation last week! Got some salt water in those pages. Also speaks to Category Theory.)

   For Category Theory:

   "The Joy of Abstraction" (2023) by Euginia Cheng

   "Basic Category Theory for Computer Scientists" by Benjamin C. Pierce

   "Conceptual Mathematics: A first introduction to categories" by Lawvere and Schanuel

   "Categories for the Working Philosopher" by Landry

   Show morethread
5. crystal_revengeAug 2025
   At least for theorem proovers like Lean, they're basically type checkers but for much more sophisticated type systems than you find in your average programming language. Basically, if the proof compiles, it is proven. In fact, if you look at Lean code it is very similar to Haskell (and the book Functional Programming with Lean is a great way to explore the language from that lens [0])

   You can also think of this in reverse and it might help you understand better: Your type checker at compile time is basically providing a sort of "proof" that all the functions and arguments in your program are consistent. Of course, because the type system is not as sophisticated, it can't prove your program is correct, but it as least can prove something about how your program will behave. If you had a more advanced type system, you could, in fact, prove more sophisticated things about the performance of your code (for example that the shapes of all your matrices matched).

   A great book on this topic is Type Theory and Formal Proof [1].

   0. https://lean-lang.org/functional_programming_in_lean/

   1. https://www.cambridge.org/core/books/type-theory-and-formal-...

   Show morethread
6. roadside_picnicJul 2025
   What's interesting about this view is that theorem provers ultimately boil down to sufficiently advanced type checking (the book Type Theory and Formal Proof is an excellent overview of this topic). Literally the heart of proof assistants like Lean is "if it compiles, you've proved it".

   So more practical type systems can be viewed as "little" theorem provers in the sense the author is describing. "Thinking in types" so to speak, is mathematically equivalent to "writing little proofs in your head". I would also add that merely using types is not equivalent to "thinking in types" as one would be required to do writing a sufficiently advanced Haskell program.

   Show morethread