Call me old fashioned, but I’m of the opinion that every “smart contract” should come with a machine-checkable proof of correctness.
You shouldn't just check against a definition Y. Ideally you'd have a set of properties that the contract must hold, then prove that X satisfies those properties. It's generally much easier to specify such properties than to write code implementing them, compare for instance an "is_sorted" function to an efficient "sort" function, so it's not just the same code written in a different language.
The issue is that how do you know you have the correct set of properties that a contract must hold? You might think you have all the properties that you need, but realize later that you missed one that is critical for your desired outcome.
This still dramatically raises the bar. EVM has a variety of very fun footguns and formal verification can help you dodge lots of these.
Solidity is much closer to being C's mentally challenged grandchild than is to javascript.
you might have an uninsured contract with multiple audits and proofs of correctness, vs an insured contract with one quick review. which one would you put money into?
Thus, eth contracts can be enforced by civil courts too, if there is some chicanery going on...
For keeps, no takebacks, no do-overs…
From the wiki page you reference for example:
> The reasoning is that a party should not be held to a contract that they were not even aware existed.
And later on, something directly relevant to this discussion perhaps:
> Mutual assent is vitiated by actions such as fraud, undue influence, duress, mutual mistake, or misrepresentation.
I think that this discussion is more closely related to the legal concept of a Mistake [0], which absolutely can be something that a court might address. Though even that doesn't seem like quite a perfect fit here.
[0] https://en.m.wikipedia.org/wiki/Mistake_(contract_law)#Mutua...
In so far as it relates to Eth, my point was that the meeting of the minds only goes as far as "the code is the contract", and the use case is to eliminate the civil courts combing over intent and who knew what.
Oh wait
A contract call that would misbehave is guaranteed to halt: not by itself, but by the EVM, which, when the contract call eventually runs out of gas, shall take care of halting it.
It's pretty nice I'd say.
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?
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.
> 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?