Software Foundations

What Hacker News says

1. BalinKingOct 2026
   IMO the experience of learning to use and understand a proof assistant gives one a pretty good foundation for then going deeper into logic and proof theory. I'm specifically thinking of Logical Foundations [0], which doubles as an introduction to Rocq and also an introduction to intuitionistic logic (and also type theory!).

   Some specific disagreements:

   - "Proof trees" on Wikipedia redirects to the page for analytic tableaus, which I don't think is particularly relevant to Lean. I think natural deduction [1] would be infinitely more useful.

   - Why is Gödel incompleteness necessary for one to understand how Lean works?

   - Why is compactness necessary knowledge? In my experience, one can use and understand any modern proof assistant without knowing anything about model theory.

   [0] https://softwarefoundations.cis.upenn.edu/lf-current/index.h..., and see also its sequel Programming Language Foundations [1].

   [1] https://softwarefoundations.cis.upenn.edu/plf-current/index....

   [1] https://en.wikipedia.org/wiki/Natural_deduction

   Show morethread
2. johnbenderOct 2026
   Lamport’s book and or Hillel Wayne’s are both good. State machines as a specification language has always been pretty approachable and also relatively deep. If you want to get in to proof assistants Software Foundations is great and the delta to understanding Lean from Rocq is pretty small.

   https://lamport.azurewebsites.net/tla/book.html https://logicforprogrammers.com/ https://softwarefoundations.cis.upenn.edu/

   thread
3. schonfinkelApr 2026
   For those unaware, one of the best resources to learn Rocq: https://softwarefoundations.cis.upenn.edu/
   thread
4. JtsummersJul 2025
   > Why don't they make it less "hard" by allowing the use of a good proof-oriented programming language [emphasis added]

   Who's preventing this now? Take a look at things like Software Foundations and other works which are built on automated or interactive proof systems.

   https://softwarefoundations.cis.upenn.edu/

   thread
5. schonfinkelJun 2025
   Highly recommend this as well. Michael Ryan also has a playlist where he goes over the first book of the "Software Foundations" series:

   https://www.youtube.com/playlist?list=PLre5AT9JnKShFK9l9HYzk... https://softwarefoundations.cis.upenn.edu/

   A great resource for those looking to learn Rocq.

   thread
6. e79Nov 2024
   If you’re interested in computer science, have you ever looked at the Software Foundations course by UPenn? It follows a similar approach of having you build all sorts of fascinating math principles and constructions from the ground up. But then it keeps going, all the way up to formal methods of software analysis and verification.

   https://softwarefoundations.cis.upenn.edu/

   thread