5 ms·
These books are surprisingly satisfying and fun to work through. The instant feedback from the proof checker makes them feel like a game of logic puzzles.
by bombastry 5y ago
These books are surprisingly satisfying and fun to work through. The instant feedback from the proof checker makes them feel like a game of logic puzzles.
- amw-zero 5y agoThere’s another book, Concrete Semantics, that starts off by saying something along the lines of: “Be careful - interactive theorem proving is addicting.” It’s so true. You can end up ‘accidentally’ proving things, and when the proof checker accepts the proof it’s a big endorphin rush. http://concrete-semantics.org/ http://concrete-semantics.org/