Verified Functional Programming in Agda is the best Agda resource available, but studying Idris via Type-driven Development with Idris will net you very transfe

Verified Functional Programming in Agda is the best Agda resource available, but studying Idris via Type-driven Development with Idris will net you very transferable insights. These are research languages, so the ideas are extremely interesting but not production ready. What I like about working in Agda is: proofs are verified by the compiler (so I know when I've proved enough), dependent types blurs the lines between types and values in a way that makes expressing complex typing relations no bother at all, and that mixfix operators let you create some really neat syntax. (Aspiring) computer scientists will be well of taking a look.