I have found Type-Driven Development with Idris [1] is a nice introduction into verifiable programming. The book starts with basic functional programming (Idris

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-idris https://www.manning.com/books/type-driven-development-with-i...