3 ms·

"The Limits of Correctness" (1985) by Bryan Cantwell Smith: https://www.student.cs.uwaterloo.ca/~cs492/11public_html/p18-smith.pdf https://www.student.cs.uwat

by jasode 9y ago

"The Limits of Correctness" (1985) by Bryan Cantwell Smith: https://www.student.cs.uwaterloo.ca/~cs492/11public_html/p18-smith.pdf https://www.student.cs.uwaterloo.ca/~cs492/11public_html/p18... I know Thompson's "Reflections on Trust" and Shannon's "Communication" papers are more famous but I believe BCS's "Correctness" paper has more immediate relevance to a wider population of programmers. For example, I don't believe Ethereum's creator, Vitalik Buterin, is familiar with it because if he was, he would have realized that "code is law" is not possible and therefore he would have predicted the DAO hack and subsequent fork/reversal to undo the code. Seriously, if you read BCS's paper and generalize its lessons learned, you will see that the DAO hack and its reversal as inevitable.

catnaroek 9y ago
> you will see that the DAO hack and its reversal as inevitable. Honest naïve question. What's the proof?
- throwawayjava 9y ago
  FWIW I think this is a very fair question. Parent's post veers a bit further toward defeatism than I think Smith's paper advocates for or justifies. In particular, of course the DAO hack wasn't inevitable -- a more careful programmer could've foreseen and prevented that attack and whole other classes of attack.
  - tom_mellior 9y ago
    Part of the linked paper's point is that because computer systems involve many "levels of failure", even a more careful programmer cannot usually rule out every class of programs. The DAO hack, yes, possibly. But, for example, people have also lost money due to bugs in the Solidity compiler: https://np.reddit.com/r/ethtrader/comments/5foa5p/daily_discussion_30nov2016/dalxys1/ https://np.reddit.com/r/ethtrader/comments/5foa5p/daily_disc... How many "more careful" Ethereum programmers also check the compiler for correctness? Another paper in this vein is James Fetzer's "Program Verification: The Very Idea". http://lore.ua.ac.be/Teaching/SSPEC2LIC/critique2.pdf http://lore.ua.ac.be/Teaching/SSPEC2LIC/critique2.pdf
    - throwawayjava 9y ago
      > Part of the linked paper's point is that because computer systems involve many "levels of failure", even a more careful programmer cannot usually rule out every class of programs. But -- and this is the crucial point -- that doesn't mean we shouldn't strive to be better than we are now. The impossibility of perfectly modeling the world hasn't prevented us from making enormous progress on software safety and security over the past 30 odd years. Today, if you care to, you can easily write code that is free of buffer overflows and command injection attacks. In the 00's SQL injection attacks were extremely easy to find; now they're comparatively rare. Smith's paper tells us that code-as-law is probably a bad idea. But it is not -- and wasn't intended to be -- an indict of static analysis or model-based engineering more generally. Every structural engineer knows the difference between a bridge and a model of a bridge; a paper pointing out the difference without substantively critiquing the practical usefulness of a particular type of model would probably elicit eye-rolls. I'm not sure why these mundane observations receive such attention in computer science. Maybe because with software the model and the system look so similar. But to be sure, the impossibility of codifying human morality is a pretty lame excuse for failing to use static analysis tools or better languages or quality frameworks to prevent known classes of attacks. So I doubt that's what Smith is advocating. > How many "more careful" Ethereum programmers also check the compiler for correctness? Yes, we should obviously check compilers for correctness, and we're making slow but sure progress toward a world where our critical infrastructure comes with strong -- of course, never perfect -- correctness guarantees.
      - tom_mellior 9y ago
        > But -- and this is the crucial point -- that doesn't mean we shouldn't strive to be better than we are now. Agreed! And I also agree that we are really making progress. But we're far from a world where people can crank out provably correct code (let alone the proofs). > I'm not sure why these mundane observations receive such attention in computer science. Maybe because with software the model and the system look so similar. Excellent point, and yes, I think that is the problem. Modeling the world in code is not much different from... er... modeling the world in code :-)
    - 9y ago
  - KirinDave 9y ago
    Given how bad the tooling is for Eth right now, it probably was inevitable. Their tooling isn't just a mess semantically and syntactically, it's was riddled with double-operation bugs.
    - deleted 9y ago
      [deleted]
LeanderK 9y ago
i enjoyed skimming the paper, but i don't agree to your conclusions. It reminds me of an recent discussion i had about Dependent Types in Haskell, why not just check for termination instead of asserting it (I know about the halting problem)? I think for many applications there is no binary answer, it's not just a good or bad idea. The question is how good can we get and is it any better than the state of the art? There are theoretical limits, but the interesting part is whether there exists a practical approximation. I don't believe in a fundamental difference between us and computers, i think everything we can reason about should be possible to algorithmically reason about. I think smart-contracts are a fundamental improvement over "non-code as law", i really believe in them. They are reproducible and exact. But it's a shame that solidity is so badly engineered, because they it is really hard to prove anything in it. I think they did the exact opposite of what would be the right language. I understand the reasoning behind "the limits of correctness", but does this means that proving anything is meaningless? I would expect most contracts to be stupidly simpel, at least to a machine, with simpel properties that need to be proven comparable to testing Haskell with quickcheck. And i believe they are an improvement over "non-code as law", even if not provably correct. The problem with bugs and smart-contracts is interesting. But implementing smart-contracts does not mean automating the judge.

by jasode 9y ago

catnaroek 9y ago

> you will see that the DAO hack and its reversal as inevitable. Honest naïve question. What's the proof?

throwawayjava 9y ago
FWIW I think this is a very fair question. Parent's post veers a bit further toward defeatism than I think Smith's paper advocates for or justifies. In particular, of course the DAO hack wasn't inevitable -- a more careful programmer could've foreseen and prevented that attack and whole other classes of attack.
- tom_mellior 9y ago
  Part of the linked paper's point is that because computer systems involve many "levels of failure", even a more careful programmer cannot usually rule out every class of programs. The DAO hack, yes, possibly. But, for example, people have also lost money due to bugs in the Solidity compiler: https://np.reddit.com/r/ethtrader/comments/5foa5p/daily_discussion_30nov2016/dalxys1/ https://np.reddit.com/r/ethtrader/comments/5foa5p/daily_disc... How many "more careful" Ethereum programmers also check the compiler for correctness? Another paper in this vein is James Fetzer's "Program Verification: The Very Idea". http://lore.ua.ac.be/Teaching/SSPEC2LIC/critique2.pdf http://lore.ua.ac.be/Teaching/SSPEC2LIC/critique2.pdf
  - throwawayjava 9y ago
    > Part of the linked paper's point is that because computer systems involve many "levels of failure", even a more careful programmer cannot usually rule out every class of programs. But -- and this is the crucial point -- that doesn't mean we shouldn't strive to be better than we are now. The impossibility of perfectly modeling the world hasn't prevented us from making enormous progress on software safety and security over the past 30 odd years. Today, if you care to, you can easily write code that is free of buffer overflows and command injection attacks. In the 00's SQL injection attacks were extremely easy to find; now they're comparatively rare. Smith's paper tells us that code-as-law is probably a bad idea. But it is not -- and wasn't intended to be -- an indict of static analysis or model-based engineering more generally. Every structural engineer knows the difference between a bridge and a model of a bridge; a paper pointing out the difference without substantively critiquing the practical usefulness of a particular type of model would probably elicit eye-rolls. I'm not sure why these mundane observations receive such attention in computer science. Maybe because with software the model and the system look so similar. But to be sure, the impossibility of codifying human morality is a pretty lame excuse for failing to use static analysis tools or better languages or quality frameworks to prevent known classes of attacks. So I doubt that's what Smith is advocating. > How many "more careful" Ethereum programmers also check the compiler for correctness? Yes, we should obviously check compilers for correctness, and we're making slow but sure progress toward a world where our critical infrastructure comes with strong -- of course, never perfect -- correctness guarantees.
    - tom_mellior 9y ago
      > But -- and this is the crucial point -- that doesn't mean we shouldn't strive to be better than we are now. Agreed! And I also agree that we are really making progress. But we're far from a world where people can crank out provably correct code (let alone the proofs). > I'm not sure why these mundane observations receive such attention in computer science. Maybe because with software the model and the system look so similar. Excellent point, and yes, I think that is the problem. Modeling the world in code is not much different from... er... modeling the world in code :-)
  - 9y ago
- KirinDave 9y ago
  Given how bad the tooling is for Eth right now, it probably was inevitable. Their tooling isn't just a mess semantically and syntactically, it's was riddled with double-operation bugs.
  - deleted 9y ago
    [deleted]

LeanderK 9y ago

i enjoyed skimming the paper, but i don't agree to your conclusions. It reminds me of an recent discussion i had about Dependent Types in Haskell, why not just check for termination instead of asserting it (I know about the halting problem)? I think for many applications there is no binary answer, it's not just a good or bad idea. The question is how good can we get and is it any better than the state of the art? There are theoretical limits, but the interesting part is whether there exists a practical approximation. I don't believe in a fundamental difference between us and computers, i think everything we can reason about should be possible to algorithmically reason about. I think smart-contracts are a fundamental improvement over "non-code as law", i really believe in them. They are reproducible and exact. But it's a shame that solidity is so badly engineered, because they it is really hard to prove anything in it. I think they did the exact opposite of what would be the right language. I understand the reasoning behind "the limits of correctness", but does this means that proving anything is meaningless? I would expect most contracts to be stupidly simpel, at least to a machine, with simpel properties that need to be proven comparable to testing Haskell with quickcheck. And i believe they are an improvement over "non-code as law", even if not provably correct. The problem with bugs and smart-contracts is interesting. But implementing smart-contracts does not mean automating the judge.