This book got me interested in what expressive types can do for software development, maintenance, etc. While I never built anything real with Idris, I did love the programming approach versus that of Coq; I was able to express some type declarations that not only enforced a semantic correctness property, but also a worst-case runtime for the implementation.

I hope to see languages like Idris become more real-world useful, and more popular languages improve the expressiveness of their type systems.