The kinds of errors where you have a type mismatch are wholly uninteresting in my experience, and get caught very early on in the development process. What I really care about is semantic correctness.
For example, consider a sort function. The types can tell me that I passed in a collection of a particular type and I got a collection of the same type back. However, what I really want to know is that the collection contains the same elements, and that they’re in order. This is difficult to express using most type systems out there. Even when the type system is powerful enough to encode such semantics, it's both difficult to figure out how to express and understand the resulting specification.
I was curious about your example of expressing and validating that a sort function returns a sorted list using the type system. I found this paper [0] by McBride, McKinna, and Altenkirch about using dependent types in the language Epigram to do exactly that. I have only scanned it, and it remains to be seen if it truly is too "difficult to figure out how to express or understand the resulting specification." Hopefully with more research it will only become easier!
The fact that it's a research topic really says all you need to know in my opinion. It's not a question of whether you can do it in principle, but rather whether it's an effective alternative to other approaches.
I agree, I don’t think dependent typing and validating the correctness of your program using formal proofs is ready for mainstream adoption. I think it might be ready for some domains, like aeronautics, where the cost of errors is very high.
It's not a question of whether you can do it in principle or not. My point was that I don't think it's an effective approach for creating such specifications compared to the alternatives such as runtime contracts.
Why is that? In fact, I would argue you want both. You want to use a contract to check the incoming data, but once it's been checked, you'd want to wrap it in a type that guarantees the property is set.
Otherwise, you have to iterate over a potentially very large set of data to check if it's sorted every time you want to use a function that has that contract.
For example, consider a sort function. The types can tell me that I passed in a collection of a particular type and I got a collection of the same type back. However, what I really want to know is that the collection contains the same elements, and that they’re in order. This is difficult to express using most type systems out there. Even when the type system is powerful enough to encode such semantics, it's both difficult to figure out how to express and understand the resulting specification.