I started with Certified Programming with Dependent Types (http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/). If you are more interested in progra

I started with Certified Programming with Dependent Types (http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/). If you are more interested in programming, consider trying Idris (http://idris-lang.org/ http://idris-lang.org/). Edwin Brady, the language designer, wrote a great book that I would recommend called Type-Driven Development with Idris (https://www.manning.com/books/type-driven-development-with-idris https://www.manning.com/books/type-driven-development-with-i...).