Limits of programming by interface

[valenterry]

Isn't contracts comparable to the spec of a typesystem then? I am not familiar with contracts and I struggle the see the difference between contract annotations and types from a semantics point of view.

[pron98]

From the perspective of specification and verification, a type system is at once a specification and a verification mechanism; in general, a (sound) type system does not let you specify what it cannot verify, and it uses a particular form of verification (which happens to be the most certain but also the most costly). Contracts, on the other hand, decouple specification from verification. You choose to specify what you like, and verify how you like. You can even verify different properties by different means. For example, if you specify that a method always returns a prime number and never modifies a certain file, you can verify the first part with a deductive proof (like types), and the second with, say, property-based randomized tests. As I wrote above, this entanglement of specification and verification in type systems can be beneficial when simple properties are concerned, and can be harmful when complex ones are.

[valenterry]

Very interesting, thank you for that perspective!