[mostlylurks]

Preconditions and postconditions seem like the wrong way to go about solving the issue they try to solve. They are essentially a secondary type system that tries to express information not expressed by the primary type system in a way that is awkwardly disconnected from the primary type system. You could instead just implement the functionality needed to incorporate that information into the primary type system. In practice this would result in an implementation of dependent types, which is fine.

[kaba0]

> implementation of dependent types, which is fine.

Which you have to prove, which is absolutely non-trivial. I guess it could be made into a runtime check as well where static analysis is not possible, but that seems to be a quite hard to reason about language regarding performance.

[mycall]

.NET Code Contracts has both compile time and runtime checks, although it always felt like a bolted on solution even though it is baked into the framework. I guess this is why it didn't carry forward into the .NET Core rewrite.

[HacklesRaised]

Betrand Meyer is coming for you... ;-)

He's not, he would respect your opinion, but design by contract was on of the key foundations of Eiffel, and I have a soft spot for Eiffel.

[throwawaymaths]

Maybe you don't have to encode everything in the type system?

Also: Maybe not everything goes in the compiler?