lylecubed

This is exactly what I'm looking for. Thanks!

This. Thank you. I'm being rate limited, so this is the only post I'll be making on this thread. My question was genuine. I want to learn both the positives and the pitfalls of dependent types. I mimicked the book's description because it amused me from a linguistic perspective. Looking back, I probably should have phrased it differently.

You just described two errors that do actually happen and in the next sentence say those errors can't happen anymore. What am I missing here?

> An introduction to dependent types, demonstrating the most beautiful aspects, one step at a time.

Is there a companion book detailing the ugly downsides of dependent types and how to avoid them, one step at a time?

> why do folks completely avoid a language for a single relatively bland syntactic feature?

Personal preference isn't a good enough reason?

I don't like white space sensitive languages because I've seen what happens in python when somebody accidentally adds a couple of lines formatted with spaces into a file formatted with tabs. I've seen git and svn mangle tabs. Long blocks are harder to track. Refactoring functions and nested ifs are much harder to keep track of. If you somehow lose all of the formatting in a block or a file, it's much more difficult to recreate the code if the only block delimiters are whitespace.

Essentially, white space delimiters are just one more thing that can go wrong and ruin my day. I try to keep those to a minimum. That said, Nim is my new go to for short scripts. I wouldn't write anything large in it for the reasons mentioned above.

Embedded development.