I read this book twice, one of my favorite reads. If you can look past the student-teacher discussion format (which I personally enjoy) it's an excellent introduction to dependent types.
I'm a fan of "The Little X" series so I bought this one when it just came out.<p>I believe the author did tried their best and a great job they did - which made me work through half of the book (which is a lot for me, and for this topic). However, I did gave up eventually and decide to revisit it in the long future.<p>My guess is people should discuss more about dependent types - I remember functional programming concepts were also hard for me as well. But after being exposed to those conversations for a while (functional programming was one of the hot topic a dacade ago), I find those concepts were not that hard to understand, they're just different from C-like's perspective.