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

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?