I've heard good things about Certified Programming with Dependent Types (http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/). "This is the web site

I've heard good things about Certified Programming with Dependent Types (http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/). "This is the web site for a textbook about practical engineering with the Coq proof assistant. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation." Edit: There's some comparison of CPDT and SF here: https://lobste.rs/s/c3lj14/certified_programming_with_dependent_types_by_adam_chlipala https://lobste.rs/s/c3lj14/certified_programming_with_depend....