It's generally (or maybe universally) more difficult to "get" dependent typing than plain old ML-family static typing. I mean, this HN comments page alone has multiple threads where people don't think that the "x > y" proof example even works. For most programmers, that's how non-obvious the possibility of proving nontrivial properties of code is. Maybe I should change the wording in the OP to make it clear that I'm talking about the set of ideas required to use the language, not the characters that need to be typed into a computer to make it work.