4 ms·

Notice that sprinkled throughout your multiple comments, you're hedging your position to provide some wiggle room: "would catch _most_ heists like this" "2% h

by 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

> 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.