Finished this book yesterday, it’s pretty good! However, I feel Dependent Types weren’t a good fit for this series’ format. This series never talks about theory except obliquely. For example, page 175 talks about the Curry-Howard correspondence and the rest of the book elaborates on it by writing proofs of various things but it’s never mentioned by name. A lot of other interesting facts were mentioned but I have no way of looking them up! This is a fine format if you’re learning Scheme, there’s not much theory there, but I feel like dependent types should have been treated differently. I’ve now been shown some examples of what you can do with dependent types but I’m still very unclear as to what they actually are, the book never explained!
I think Typed Racket could be a good contender for the demonstration language but I’m guessing they made up an ad hoc language for simplicity.