I could recommend Coq Art: http://www.labri.fr/perso/casteran/CoqArt/ http://www.labri.fr/perso/casteran/CoqArt/ Unfortunately, formal proofs are very theoretic

I could recommend Coq Art: http://www.labri.fr/perso/casteran/CoqArt/ http://www.labri.fr/perso/casteran/CoqArt/ Unfortunately, formal proofs are very theoretical and there's a lot of concepts to learn that aren't found in regular programming. This book eases you into things though.