4 ms·

Simple, just declare any and all consequences of the contract to be binding and it is now correct by definition.

tgv 5y ago
That's very well possible, and a desirable property of such contracts. It does restrict the language in which contracts must be written.
- contravariant 5y ago
  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?
  - ImprobableTruth 5y ago
    >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.
  - tgv 5y ago
    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?
MontagFTB 5y ago
In those cases there are no remedies for bugs. What recourse does a victim have in the case of an exploit? How is such a system supposed to attract users when there are no guarantees that problems will ever resolve in their favor?
swamp40 5y ago
Like the Pope.

tgv 5y ago

That's very well possible, and a desirable property of such contracts. It does restrict the language in which contracts must be written.

contravariant 5y ago
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?
- ImprobableTruth 5y ago
  >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.
- tgv 5y ago
  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?

MontagFTB 5y ago

In those cases there are no remedies for bugs. What recourse does a victim have in the case of an exploit? How is such a system supposed to attract users when there are no guarantees that problems will ever resolve in their favor?

swamp40 5y ago

Like the Pope.