I love math and a good type system. I know little about formal verification of code. Are there tools (ideally) or languages (for educational, if not production, use) you recommend I look at?
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/