11 ms·

Call me old fashioned, but I’m of the opinion that every “smart contract” should come with a machine-checkable proof of correctness.

casi18 5y ago
I think we will see more work like this, and tools developed to help. but really it comes down to tradeoffs of speed and security, what cant be insured, and the impact of bugs. 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?
- nicoburns 5y ago
  Neither? I'd much rather use a traditional contract that can fallback on the legal system if need be.
  - bbarnett 5y ago
    A handshake can be a binding contract. Words spoken can bind you. Thus, eth contracts can be enforced by civil courts too, if there is some chicanery going on...
    - dsr_ 5y ago
      ...as long as all the participants are traceable entities with known legal jurisdictions.
    - jacquesm 5y ago
      Yes, but that would invalidate a very large chunk of the possible usecases for eth contracts. After all, if you end up needing the courts anyway you might as well use a normal contract, and the whole advantage of eth contracts - to me at least - appears to be the feature that the eth contract is the entirety of the arrangement. So it can be used between two parties in entirely different jurisdictions without that creating an imbalance.
      - deleted 5y ago
        [deleted]
    - jameshart 5y ago
      And when the court orders that the parties do something that the eth contract cannot permit (and has been formally proven to prevent from ever being induced to do), how does the eth contract handle that?
    - JackFr 5y ago
      If the meeting of the minds [1] is that the code is the contract, then the civil courts aren’t going to help. For keeps, no takebacks, no do-overs… [1] https://en.m.wikipedia.org/wiki/Meeting_of_the_minds https://en.m.wikipedia.org/wiki/Meeting_of_the_minds
      - tomalpha 5y ago
        IANAL, but I understood Meeting Of Minds to refer to the need for both parties to a contract to actually agree that a contract exists. 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)#Mutual_mistake https://en.m.wikipedia.org/wiki/Mistake_(contract_law)#Mutua...
        JackFr 5y ago
        IANAL either but my understanding was that the "meeting of the minds", is not just that a mutual understanding that contract exists but there is an agreement on basis of the contract. 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.
antupis 5y ago
I think it is moving there but ecosystem is not there yet. Also it does not help that Ethereum has chosen Solidity which is bastard child of javascript.
- m00dy 5y ago
  would you elaborate on solidity vs js ?
  - antupis 5y ago
    https://docs.soliditylang.org/en/v0.8.7/language-influences.html https://docs.soliditylang.org/en/v0.8.7/language-influences.... there is still strong resemble between js and solidity.
    - m00dy 5y ago
      I think it is only "function" keyword. I'm not sure how strong resemble is.
- tiborsaas 5y ago
  It's more similar to Java or TypeScript than JavaScript.
- danielvf 5y ago
  Solidity has very very little in common with javascript other than they were both quickly put together languages full of weird spots, and both fairly successful. Solidity is much closer to being C's mentally challenged grandchild than is to javascript.
PeterisP 5y ago
The problem is with how you define and describe "correctness" - a machine can check that code X matches definition Y, but there can be bugs in the nuances of that formal definition Y, so you effectively just have a different set of code in a different language (that formal definition) that you need to audit.
- logicchains 5y ago
  >a machine can check that code X matches definition Y 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.
  - dannyw 5y ago
    A "is_facebook" function may not be much easier. Smart contracts like Compound, Uniswap are complex functions; much more complicated than sorting which has an objectively correct answer.
    - goldenkey 5y ago
      We can do a probabilistic check. Just see how much data is being exfiltrated, if it's greater than a X% we can figure it's either Facebook or the Chinese government. ;-)
  - cortesoft 5y ago
    > Ideally you'd have a set of properties that the contract must hold, then prove that X satisfies those properties. 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.
    - 5y ago
elif 5y ago
First, start with an automatic proof that the contract will halt... Oh wait
- WJW 5y ago
  You jest, but the halting problem is only unsolvable in the general case. For "most" (but not all) programs it is perfectly possible to prove whether or not they will halt.
  - carnitine 5y ago
    Most real world programs, not most programs in general.
- TacticalCoder 5y ago
  The halting problem in Ethereum is "solved" (more like "dealth with") by a very simple technique: every EVM instruction has a cost and you have to provide "gas" to run your smart contract. If you don't provide enough gas, your contract call has zero effect and all the gas you paid is lost. 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.
  - mst 5y ago
    IIRC erlang does reduction based scheduling except with a multiplier related to the number of messages in its mailbox - would be interesting to read a comparison from somebody who understands the runtimes better than I do.
- mbrodersen 5y ago
  Easy. Just use a language that isn’t Turing complete or require a proof of termination. All solved problems in the proof community.
contravariant 5y ago
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?
anm89 5y ago
why be absolutist? is that necessary if the contract has $20 riding on it?

casi18 5y ago

I think we will see more work like this, and tools developed to help. but really it comes down to tradeoffs of speed and security, what cant be insured, and the impact of bugs. 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?

nicoburns 5y ago
Neither? I'd much rather use a traditional contract that can fallback on the legal system if need be.
- bbarnett 5y ago
  A handshake can be a binding contract. Words spoken can bind you. Thus, eth contracts can be enforced by civil courts too, if there is some chicanery going on...
  - dsr_ 5y ago
    ...as long as all the participants are traceable entities with known legal jurisdictions.
  - jacquesm 5y ago
    Yes, but that would invalidate a very large chunk of the possible usecases for eth contracts. After all, if you end up needing the courts anyway you might as well use a normal contract, and the whole advantage of eth contracts - to me at least - appears to be the feature that the eth contract is the entirety of the arrangement. So it can be used between two parties in entirely different jurisdictions without that creating an imbalance.
    - deleted 5y ago
      [deleted]
  - jameshart 5y ago
    And when the court orders that the parties do something that the eth contract cannot permit (and has been formally proven to prevent from ever being induced to do), how does the eth contract handle that?
  - JackFr 5y ago
    If the meeting of the minds [1] is that the code is the contract, then the civil courts aren’t going to help. For keeps, no takebacks, no do-overs… [1] https://en.m.wikipedia.org/wiki/Meeting_of_the_minds https://en.m.wikipedia.org/wiki/Meeting_of_the_minds
    - tomalpha 5y ago
      IANAL, but I understood Meeting Of Minds to refer to the need for both parties to a contract to actually agree that a contract exists. 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)#Mutual_mistake https://en.m.wikipedia.org/wiki/Mistake_(contract_law)#Mutua...
      - JackFr 5y ago
        IANAL either but my understanding was that the "meeting of the minds", is not just that a mutual understanding that contract exists but there is an agreement on basis of the contract. 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.

antupis 5y ago

I think it is moving there but ecosystem is not there yet. Also it does not help that Ethereum has chosen Solidity which is bastard child of javascript.

m00dy 5y ago
would you elaborate on solidity vs js ?
- antupis 5y ago
  https://docs.soliditylang.org/en/v0.8.7/language-influences.html https://docs.soliditylang.org/en/v0.8.7/language-influences.... there is still strong resemble between js and solidity.
  - m00dy 5y ago
    I think it is only "function" keyword. I'm not sure how strong resemble is.
tiborsaas 5y ago
It's more similar to Java or TypeScript than JavaScript.
danielvf 5y ago
Solidity has very very little in common with javascript other than they were both quickly put together languages full of weird spots, and both fairly successful. Solidity is much closer to being C's mentally challenged grandchild than is to javascript.

PeterisP 5y ago

The problem is with how you define and describe "correctness" - a machine can check that code X matches definition Y, but there can be bugs in the nuances of that formal definition Y, so you effectively just have a different set of code in a different language (that formal definition) that you need to audit.

logicchains 5y ago
>a machine can check that code X matches definition Y 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.
- dannyw 5y ago
  A "is_facebook" function may not be much easier. Smart contracts like Compound, Uniswap are complex functions; much more complicated than sorting which has an objectively correct answer.
  - goldenkey 5y ago
    We can do a probabilistic check. Just see how much data is being exfiltrated, if it's greater than a X% we can figure it's either Facebook or the Chinese government. ;-)
- cortesoft 5y ago
  > Ideally you'd have a set of properties that the contract must hold, then prove that X satisfies those properties. 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.
  - 5y ago

elif 5y ago

First, start with an automatic proof that the contract will halt... Oh wait

WJW 5y ago
You jest, but the halting problem is only unsolvable in the general case. For "most" (but not all) programs it is perfectly possible to prove whether or not they will halt.
- carnitine 5y ago
  Most real world programs, not most programs in general.
TacticalCoder 5y ago
The halting problem in Ethereum is "solved" (more like "dealth with") by a very simple technique: every EVM instruction has a cost and you have to provide "gas" to run your smart contract. If you don't provide enough gas, your contract call has zero effect and all the gas you paid is lost. 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.
- mst 5y ago
  IIRC erlang does reduction based scheduling except with a multiplier related to the number of messages in its mailbox - would be interesting to read a comparison from somebody who understands the runtimes better than I do.
mbrodersen 5y ago
Easy. Just use a language that isn’t Turing complete or require a proof of termination. All solved problems in the proof community.

contravariant 5y ago

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?

anm89 5y ago

why be absolutist? is that necessary if the contract has $20 riding on it?