A recent book in the same vein: The Hitchhiker's Guide to Logical Verification https://github.com/blanchette/logical_verification_2020 https://github.com/blanc

A recent book in the same vein: The Hitchhiker's Guide to Logical Verification https://github.com/blanchette/logical_verification_2020 https://github.com/blanchette/logical_verification_2020 This is a tipping point work making the case that type theory is like a musician reading sheet music. Sure, the Beatles couldn't, but... Anyone developing a new programming language should understand languages at the level of Lean, even if the common uses of their constructs aren't theorem proving. The analogies are mind-blowing. Monadic parsing is the same thing as meta-programming tactics? I'm still wrapping my head arond that one.