>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.
That's a test though -- and a contract is basically an assertion for such a test.
Types allow you to express and check things before the code is run.
The question isn't whether you can do something in principle. It's whether the approach is more effective than alternatives. My experience is that it's not.
>It's whether the approach is more effective than alternatives. My experience is that it's not.
It obviously is more effective, since you can prove parts of your programs behavior throughout at compile time -- whereas contracts depend on passing through some particular code.
Besides those are two different things. You can have types to do the heavy lifting AND contracts a la e.g. Eiffel
It's only obviously more effective coming from a very narrow perspective. Static typing can provide stronger guarantees, but if it takes significantly more effort to do that and you already get adequate guarantees with contracts then that effort is likely not justified.
The goal is typically to ship software that works well enough in a reasonable amount of time, and my experience is that contracts provide a much better tool for doing that.
While contracts need to execute the code, generative testing provides you with a sufficient sample to be reasonably sure that the code is doing what you want. The contracts also let you directly specify what the code is intended to be doing, something that's not easy to do using the type system.
In some situations proving parts of the program behavior may be worth the effort, but I simply don't agree that it's true for the general case.
That's a test though -- and a contract is basically an assertion for such a test.
Types allow you to express and check things before the code is run.