If you're looking to do some dependently-typed programming and theorem proving, Coq is perhaps the most mature tool to learn. It's actually two different langu

If you're looking to do some dependently-typed programming and theorem proving, Coq is perhaps the most mature tool to learn. It's actually two different languages, Gallina, which is what is shown in OP, and Ltac, which is the tactic language. I enjoyed Software Foundations[1], which, if you have the time, lets you self-study theorem proving starting from scratch. Somewhat less known is the book Formal Reasoning About Programs[2] which is more advanced but informative as well. [1] https://softwarefoundations.cis.upenn.edu/lf-current/index.html https://softwarefoundations.cis.upenn.edu/lf-current/index.h... [2] http://adam.chlipala.net/frap/ http://adam.chlipala.net/frap/