Well it's not technically a restriction, though it'd be a lot easier if you wrote contracts in a language that left no room for doubt certainly.

In fact you can't really get away from the need for a clear formal description of what the contract does anyway. If you write it in a more flexible language but only accept it with a proof of some formal properties then those formal properties are in effect the contract.

At which point we reach something I still don't quite understand. If people accept code satisfying those formal properties as 'proven correct', then why aren't the contracts written as those formal properties in the first place?

>then why aren't the contracts written as those formal properties in the first place?

How are you going to enforce the contract? If it's formally verified, the contract is enforced by itself.

Not to mention, I think as a developer accepting a spec that isn't verified is a tough pill to swallow, because any bug no matter the size would mean that you're breaking the contract.

It's a restriction, even if it turns out to be a 95% subset of C, because without restrictions, the halting problem would prevent effective verification.

> In fact you can't really get away from the need for a clear formal description of what the contract does anyway.

The code is its own description. The point is verification: does the code implement the contract?