alt Hacker NewsPoor man's runtime "dynamic" version. AKA: A much worse version.
In advanced cases, you'd need dependent types, but the only place where that almost shows up is in the "amount <= balance" assertions. That's also silly because if you typed "amount" and "balance" correctly, then "balance -= amount" has to produce a runtime error because the resulting balance would be negative and not a valid value for the type. So, it's a very natural place anyway to force the programmer to properly handle errors anyways.
"Contracts" has been around a long time and has not caught on. That's usually a good sign that better approaches are prevailing.
In other words: refinement types are a better solution.
Replies
> Poor man's runtime "dynamic" version. AKA: A much worse version.
Contracts don't have to be evaluated dynamically, that's just one way they're implemented. See SPARK/Ada for an example of contracts being used to prove programs statically, not just test them dynamically.
contract is way wider than simple refinement types. Refinement types are just a very specific group of invariants.
Contracts are an attempt to include formal specification languages into the implementation languages. You can enforce valid and invalid state changes, enforce relationships across the program state, or even enforce some level of correctness in behaviour.
> around a long time and has not caught on. That's usually a good sign that better approaches are prevailing.
That is completely not true. Plenty of dumb things prevail for faar too long for no other reason than momentum. Plenty of great things remain academic forever. It took decades to get algebraic types or basic functional programming somewhat accepted.
Design by contract is in theory a good idea but suffers from being a pain to use effectively. (making actually useful invariants that help the program more than an assert already would have)
Adding them to languages not built around them also results in quite nasty boilerplate or runtime overhead which further discourage their usage.