I went through Benjamin Pierce et. al - Logical Foundations [0] which uses Coq. It was great fun, and I am someone who has a pattern of shying away from mathema

I went through Benjamin Pierce et. al - Logical Foundations [0] which uses Coq. It was great fun, and I am someone who has a pattern of shying away from mathematics a little too often. That said, I'm not the right person to tell you why and when Coq > all other proof systems. Pierce is famous though, and so are his books. [0] https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/