4 ms·

>I think you'd agree that a 2% heist is better than a 60% heist. Sure, but I was talking about a much more rigorous standard than "2% better than 60%" because

by jasode 10y ago

>I think you'd agree that a 2% heist is better than a 60% heist. Sure, but I was talking about a much more rigorous standard than "2% better than 60%" because the author Jon Evans wrote: ""In principle, code can be proved _correct _ with formal verification."" I'm not sure he understands what "correct" actually means. If Mr Evans is framing "correct" in the sense of corresponding to a spec (see ahelwer's excellent comment as an example), it still doesn't solve how everybody else determines how Ethereum to behaving "correctly". (E.g. the code passed the spec checker, but it's still judged as incorrect.) Those are 2 different levels of correctness and formal verification algorithms has limited power to solve the "human judgement of correctness".

pron 10y ago
> and formal verification algorithms has limited power to solve the "human judgement of correctness". Yes, but formal methods are no more limited than any other approach, and can come closer to the ideal than anything else -- for a price. BTW, we do not usually speak of "formal verification algorithms", just as we do not usually speak of "programming algorithms" or "testing algorithms". Formal verification is a human process, akin (and complementary) to programming or testing. The general idea is that the developers express the properties they'd like the program to have in a few short formal sentences, and then the program is proven (or verified in some other way) to conform with that specification. Nothing can prevent the problem of humans failing to express what they really mean. In fact, this is a problem with contracts more than anything else, because contracts need to accommodate many contingencies, which is why I think that the whole notion of machine contracts is rather foolish. But the technical point is that the specific problem with Ethereum's heist was very clearly one of a program not conforming to (an informal) spec, that its creators had in mind.
- jasode 10y ago
  Notice that sprinkled throughout your multiple comments, you're hedging your position to provide some wiggle room: "would catch _most_ heists like this" "2% heist is _better_ than a 60% heist" ", and can come _closer_ to the ideal than anything else" However, I wasn't talking about degrees on a continuum such as "most/better/closer". I suspect that your prudent avoidance of absolutist statements actually gets to the idea I'm trying to convey. To recap, Jon Evan's asserts that Solidity can be "proved _correct_". Well, that's a boolean TRUE/FALSE instead of range of bad-to-good outcomes. >Yes, but formal methods are no more limited than any other approach, and can come closer to the ideal than anything else I'm not disagreeing with that particular statement. I'm not saying formal verfication doesn't help. It does help! I'm saying it's misapplied to the word "correct" in the sense that a mass of Ethereum users would understand that word. We are talking about 2 different levels of correctness: A) rules correctness: proven "correct" in the sense formal specification and program verification. Yes, this can be done but it will always be incomplete in how it maps to humans' idea of what is ultimately correct. B) intention correctness: proven "correct" in the sense of Solidity working the way humans would interpret as correct (I recommend reading Brian Cantwell Smith's essay on "The Limits of Correctness"[1]) To put another way, there exists an (unknown) set of programs that simultaneously satisfies both properties: 1) passed the formal verification rules with zero errors 2) judged as working incorrectly by humans which leads to a fork/reversal The existence of such programs contradicts Mr Evans statement. >Ethereum's heist was very clearly one of a program not conforming to (an informal) spec, that its creators had in mind. No it isn't clear. It sparked a deep philosophical debate. Ethereum's creators had an informal spec of the "code _IS_ the contract" and not "the code is PROVISIONAL and humans forking the code is the ultimate contract". For a vocal subset of Ethereum users, the heist did conform to their (incomplete) spec! The word "incomplete" shouldn't be in parentheses because every finite specification is incomplete against unforseen hacks. [1]https://www.student.cs.uwaterloo.ca/~cs492/11public_html/p18-smith.pdf https://www.student.cs.uwaterloo.ca/~cs492/11public_html/p18...
  - pron 10y ago
    > The existence of such programs contradicts Mr Evans statement. Yes, but only if you insist on a very strict interpretation of "correctness" as some Platonic ideal that doesn't exist. If that's what the author meant, then you're right that it is unattainable. > Ethereum's creators had an informal spec of the "code _IS_ the contract" I don't know if the word spec as it is used in formal methods is the right one here, just as I don't know if saying "they created the empty test suite" makes sense. That is a decision to treat the code as the contract, basically a decision to declare any sequence of bits as correct by definition. However, a specification as understood in formal verification is an expression of what you want the code to do. Obviously, the authors of said contract felt it failed to meet what they had in mind in writing this particular program, hence it did not conform to their imagined spec. And this is the whole point of techniques like testing or formal verification: making sure that the program does what you want it to do as much as possible.

by jasode 10y ago

pron 10y ago

> and formal verification algorithms has limited power to solve the "human judgement of correctness". Yes, but formal methods are no more limited than any other approach, and can come closer to the ideal than anything else -- for a price. BTW, we do not usually speak of "formal verification algorithms", just as we do not usually speak of "programming algorithms" or "testing algorithms". Formal verification is a human process, akin (and complementary) to programming or testing. The general idea is that the developers express the properties they'd like the program to have in a few short formal sentences, and then the program is proven (or verified in some other way) to conform with that specification. Nothing can prevent the problem of humans failing to express what they really mean. In fact, this is a problem with contracts more than anything else, because contracts need to accommodate many contingencies, which is why I think that the whole notion of machine contracts is rather foolish. But the technical point is that the specific problem with Ethereum's heist was very clearly one of a program not conforming to (an informal) spec, that its creators had in mind.

jasode 10y ago
Notice that sprinkled throughout your multiple comments, you're hedging your position to provide some wiggle room: "would catch _most_ heists like this" "2% heist is _better_ than a 60% heist" ", and can come _closer_ to the ideal than anything else" However, I wasn't talking about degrees on a continuum such as "most/better/closer". I suspect that your prudent avoidance of absolutist statements actually gets to the idea I'm trying to convey. To recap, Jon Evan's asserts that Solidity can be "proved _correct_". Well, that's a boolean TRUE/FALSE instead of range of bad-to-good outcomes. >Yes, but formal methods are no more limited than any other approach, and can come closer to the ideal than anything else I'm not disagreeing with that particular statement. I'm not saying formal verfication doesn't help. It does help! I'm saying it's misapplied to the word "correct" in the sense that a mass of Ethereum users would understand that word. We are talking about 2 different levels of correctness: A) rules correctness: proven "correct" in the sense formal specification and program verification. Yes, this can be done but it will always be incomplete in how it maps to humans' idea of what is ultimately correct. B) intention correctness: proven "correct" in the sense of Solidity working the way humans would interpret as correct (I recommend reading Brian Cantwell Smith's essay on "The Limits of Correctness"[1]) To put another way, there exists an (unknown) set of programs that simultaneously satisfies both properties: 1) passed the formal verification rules with zero errors 2) judged as working incorrectly by humans which leads to a fork/reversal The existence of such programs contradicts Mr Evans statement. >Ethereum's heist was very clearly one of a program not conforming to (an informal) spec, that its creators had in mind. No it isn't clear. It sparked a deep philosophical debate. Ethereum's creators had an informal spec of the "code _IS_ the contract" and not "the code is PROVISIONAL and humans forking the code is the ultimate contract". For a vocal subset of Ethereum users, the heist did conform to their (incomplete) spec! The word "incomplete" shouldn't be in parentheses because every finite specification is incomplete against unforseen hacks. [1]https://www.student.cs.uwaterloo.ca/~cs492/11public_html/p18-smith.pdf https://www.student.cs.uwaterloo.ca/~cs492/11public_html/p18...
- pron 10y ago
  > The existence of such programs contradicts Mr Evans statement. Yes, but only if you insist on a very strict interpretation of "correctness" as some Platonic ideal that doesn't exist. If that's what the author meant, then you're right that it is unattainable. > Ethereum's creators had an informal spec of the "code _IS_ the contract" I don't know if the word spec as it is used in formal methods is the right one here, just as I don't know if saying "they created the empty test suite" makes sense. That is a decision to treat the code as the contract, basically a decision to declare any sequence of bits as correct by definition. However, a specification as understood in formal verification is an expression of what you want the code to do. Obviously, the authors of said contract felt it failed to meet what they had in mind in writing this particular program, hence it did not conform to their imagined spec. And this is the whole point of techniques like testing or formal verification: making sure that the program does what you want it to do as much as possible.