Every discussion or article I have read on dependent types assumes that the reader is a mathematician. I usually make it only a few paragraphs in before I am completely lost.
Right now the only thing that seems clear is that dependent typing adds significant mental burden on the programmer to more thoroughly specify types, and to do so absolutely correctly. In exchange for that burden, there must be practical (not theoretical) benefits but they do not come through clearly. All of the examples I've seen are about "index of a list is guaranteed in bounds". That is such a minor and infrequent bug in practice that it does not justify the additional complexity. There must be more, that I'm just not seeing.
Is there a "Dependent types for non-mathematicians" article out there somewhere, where I can learn about patterns and practical applications?
Right now the only thing that seems clear is that dependent typing adds significant mental burden on the programmer to more thoroughly specify types, and to do so absolutely correctly. In exchange for that burden, there must be practical (not theoretical) benefits but they do not come through clearly. All of the examples I've seen are about "index of a list is guaranteed in bounds". That is such a minor and infrequent bug in practice that it does not justify the additional complexity. There must be more, that I'm just not seeing.
Is there a "Dependent types for non-mathematicians" article out there somewhere, where I can learn about patterns and practical applications?