There’s another book, Concrete Semantics, that starts off by saying something along the lines of: “Be careful - interactive theorem proving is addicting.” It’

There’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/