Coq is so much fun. It makes writing proofs feel like playing a video game. I've just finished writing a Coq tutorial [1] that is aimed at programmers (rather

Coq is so much fun. It makes writing proofs feel like playing a video game. I've just finished writing a Coq tutorial [1] that is aimed at programmers (rather than, say, computer scientists). It covers topics like programming with dependent types, writing proofs as data, universes & other type theory stuff, and extracting verified code—with exercises. [1] https://github.com/stepchowfun/proofs/tree/main/proofs/Tutorial https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor...