[mort96]

Contracts are already informally a thing: most functions have preconditions, and if you break those preconditions, the function doesn't make any guarantees of what it does.

We already have some primitive ways to define preconditions, notably the assert macro and the 'restrict' qualifier.

I don't mind a more structured way to define preconditions which can automatically serve as both documentation and debug invariant checks. Though you could argue that a simpler approach would be to "standardize" a convention to use assert() more liberally in the beginning of functions as precondition checks; that a sequence of 'assert's before non-'assert' code should semantically be treated as the functions preconditions by documentation generators etc.

I haven't looked too deep into the design of the actual final contracts feature, maybe it's bad for reasons which have nothing to do with the fundamental idea.