[schoen]

I'm curious about resources that are specifically meant to help people who've learned one proof environment learn others.

I started learning a little bit of Lean from the Natural Number Game, and subsequently worked through Logical Foundations (with the generous help of one of the coauthors!), and have continued learning Coq afterward.

Are there books or sites or exercises out there for "people who've already learned Isabelle and now would like to learn Coq", "people who've already learned Coq and now would like to learn Lean", "people who've already learned Coq and now would like to learn tools and frameworks for verifying protocols", "people who've learned OCaml or Haskell and now would like to learn Coq", etc.?

[jnash]

Have you tried Idris? It is a "practical" programming language that also gives you the full power of Dependent Types to prove your code correct. There is a great book "Type-Driven Development with Idris" that really helped me open my mind to the power of Dependent Types.

[schoen]

Yes, I'm borrowing that specific book from a friend who is really into functional programming, but I haven't read it.

It does look like Idris helps make it especially straightforward to write correct code and know when you've done so.