Concerning the books on the topic, I highly recommend this: https://www.amazon.com/Verified-Functional-Programming-Agda-... If you want to get into the math related aspect, read this: https://homotopytypetheory.org/book/

There's also an annual summer school on the topic which has downloadable videos available: https://www.cs.uoregon.edu/research/summerschool/summer17/

This year's OPLSS did not really engage with Coq. Adam Chlipala did give a lecture series on Coq at OPLSS'16 though: https://www.cs.uoregon.edu/research/summerschool/summer15/cu...

The DeepSpec summer school, however, did lead with a Coq intensive, which was recorded and included in the uploads at https://www.youtube.com/channel/UC5yB0ZRgc4A99ttkwer-dDw .

It's going to be hard to learn one way or another. Chlipala's Certified Programmimg with Dependent Types is free online. Then, Software Foundations others mentioned. Starting with lightweight stuff like Alloy or TLA+ might help. Also, The Little Prover book teaches how provers work by letting reader build a small one. Had some decent reviews.

Chlipala's book is a decent one, but it's oriented towards software verification, coq, and the use of tactics (which I would consider anti-pattern).

Software Foundations is a good introduction to Coq and proofs, but overall is quite basic, and it also hides many details of how type theory works, so it's more of a hands on tutorial.

TLA+ is just a tool which basically does its job by exhaustively searching a space of possible solutions trying to find counterexamples. It works in some limited cases but doesn't work generally for any mathematical theorem.

> TLA+ is just a tool which basically does its job by exhaustively searching a space of possible solutions trying to find counterexamples. It works in some limited cases but doesn't work generally for any mathematical theorem.

Nope. TLA+ is a rich mathematical formalism, that includes a full-fledged proof assistant. It is, however, focused on verifying software rather than arbitrary mathematical theorems. There is also a model checker for TLA+ that can check your theorems (about finite cases of programs) at the push of a button. In practice, model checkers works in more cases than manual proofs, as manual proofs "fail" much more often, simply by being far too laborious; a model checker would verify in days what may take you months or more to manually prove.

I bring up TLA+ because many people have quit trying to learn Coq because it was so hard with little perceived benefit. TLA+ has a high ratio of benefit for work put in. It also shows that abstract modeling can knock out deeper errors than regular tests or sometimes review. That makes it a nice, intermediate step toward stuff like Coq. Just a hunch a few of us have. :)

Alloy was really helpful for me to grasp the ideas behind checking a system design. But it is not a tool to write verifiable code. Rather it is a modelling tool to find bugs in the design before implementing things in code.

Software Foundations book [1] covers many case studies. One of the authors has a lecture course based around the book as well.

[1] softwarefoundations.cis.upenn.edu/current/index.html

Indeed: Benjamin Pierce's lectures on "Software Foundations in Coq" https://www.youtube.com/playlist?list=PLGCr8P_YncjUT7gXUVJWS...

I can recommend SF, I just started it a week ago without prior Coq experience. I'm using the VSCode integration which helps, CoqIDE is a bit clunky.

In Coq to Rust Program Extraction https://news.ycombinator.com/item?id=12183095 , I saw some useful comments about its foundations.

(And for a bit more about Coq to Rust, Program extraction from Coq https://github.com/rust-lang/rfcs/issues/667 )

I have found Type-Driven Development with Idris [1] is a nice introduction into verifiable programming. The book starts with basic functional programming (Idris is how a strict Haskell could look) and gradually adds dependent types and working with proofs.

[1] https://www.manning.com/books/type-driven-development-with-i...

To really learn coq, you need to learn type theory which is hidden behind tactics. IMO, Coq isn't the best way to do so. I highly recommend starting with Agda instead.

Lean hits a really good middle ground I think. More resources for Agda probably. But I'm very fond of lean ;)

Lean is very interesting, but Agda and especially Coq has more learning resource, so for the beginners it's probably better to start from them, even though, in some sense Lean is more modern.

I have the impression that for someone coming from a programming background, Idris is also a pretty good introduction to the world of dependently typed programming and proof assistants.