[amw-zero]

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/