If you're excited about that, you might enjoy https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/ Officially you're supposed

If you're excited about that, you might enjoy https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/ Officially you're supposed to download the book and then edit the exercise solutions into it with Emacs (or VSCode, I think), as you can then run the exercises to see if they type-check (i.e., if they're correct!). However, there's also a not-necessarily-up-to-date interactive in-browser version: https://jscoq.github.io/ext/sf/ https://jscoq.github.io/ext/sf/ I haven't used Idris, so I'd say it's quite possible that working through the Idris book is also just as fun and relevant for understanding the implications of the Curry-Howard correspondence.