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/Tutor...