Even the Little series covers types and proofs now:
Plus some topic-specific classics:
And some constructive foundations:
As an aside, since Coq is the only theorem proving language I know well, I am curious what the pros/cons are as compared to Isabelle/HOL, F*, Lean, etc. Coq has been around for a while, but I keep seeing new theorem provers pop up. What are the alleged weaknesses of Coq that other languages are trying to fix?
There is an additional dimension which is strength of the logic at hand. The logics Coq, Lean et al are based on are more expressive in various dimensions. Whether that's relevant to your use case depends on what kind of maths you are trying to formalise. If it is higher category theory, it matters a great deal, for program verification it tends not to be important b/c most program verification can be done in rather weak logics.
This was a while back, maybe the problem has been solved now, I have not followed this field. But as far as I'm aware, the 'hammering' approach to proof automation that has been working well with Isabelle/HOL has been successfully ported to Coq/Agda etc.
- Existing automatic theorem provers often produced non-constructive
- Existing automatic theorem provers are mostly for FOL, so the gap to
the much more powerful logics of Curry-Howard based provers is
bigger than with weaker systems.
Have both problems been solved comprehensively as of January 2020?
Yes, they use theorem provers, but proofs are optional and not required to follow the material. And they do cover those topics you mention.
If you like distributed systems, Hillel Wayne's book on TLA+ will let you see how model checking can easily spot errors that are hard to test for:
Spin has been used in similar ways for a long time:
Alloy is a model checker that has a GUI for exploring models. It's more focused on exploring structures. Their site links to a book, Software Abstractions, that will teach you a lot of concepts without needing a strong, mathematical background.
Pamela Zave used both Spin and Alloy to find errors in real-world protocols:
If focus is programming (esp low-level), SPARK Ada lets programmers annotate code with the expected behavior before that's fed into provers that confirm or refute the code operates that way in all situations. Barnes and Barnes wrote a nice book teaching both it and Praxis' Correct-by-Construction method for software development:
Many people don't make it through the stuff teaching formal proof in Coq and so on. It's really hard with few gains along the way. TLA+, SPIN, Alloy, and SPARK Ada are much more accessible with a higher work-to-reward ratio. Those easier results might justify further investment in learning the hard stuff.
Those wondering about how formal methods are used in a lot of situations might like our list on Lobsters. We have a number of professionals and enthusiasts there who stay posting both historically significant and cutting-edge work.
Some introduction https://blog.adacore.com/using-coq-to-verify-spark-2014-code (from 2014, so probably much improved since).
And some examples : http://docs.adacore.com/spark2014-docs/html/ug/gnatprove_by_...
Not the best way to learn manual proof, but I've seen it used very efficiently.
But then if course you're faced with the difficulty of increasing automation : the more you automate, the more it is difficult to have the 'muscle memory' (and lower cognitive load) that you get when flexing the manual proof often...