Finding out about how, in a programming language with dependent types, types can be returned from functions like values, feels about the same way as when I learned functions can be returned as first-class values in functional programming. It went from "wait, what?" to "of course, why wouldn't you be allowed to do that?" From seeming confusing to seeming perfectly natural, leaving you more confused of its abscence than its presence. Though admittedly, I don't have much experience with using dependent types seriously.

This property of dependent types:

> In fact, if you don't mind writing a proof or two, our sprintf function can be called on format strings that aren't fully known at compile-time! You only need to be able to prove that the string will have certain format specifiers, and then calling sprintf can typecheck.

It's not new to me, but I also find it pretty cool. Proving things at compile-time that certain runtime conditions will hold using a programming language is so much cooler than just proving it to yourself in your head or on paper, and then doing a runtime assertion in the actual code. Or, not doing a check at all, and just having crashes or security vulnerabilities if you're mistaken.