7 ms·

> The halting problem states you can't predict what a turing complete program will do, until you run it. This means to some degree, that you can't predict what

> The halting problem states you can't predict what a turing complete program will do, until you run it. This means to some degree, that you can't predict what your "smart" contract will do, until it does it. Thus turing completeness causes security to be far, far harder than non turing completeness. This is how you lose the millions of dollars as the DAO did after it passed audits. The Halting Problem states that you can't create a general purpose algorithm for predicting what an arbitrary program in a Turing Complete language will do. This is very different.

MarkPNeyer 9y ago
To elaborate: You can look at some programs with your mind, and tell quite clearly what they'll do. You can't write a _program_ that will look at other programs, and always give a correct answer.
RichardHeart 9y ago
"The naïve Ethereum people think they've cleverly sidestepped this with the notion of "gas" but actually all they're doing is cheating with this messy kludge: because simply saying "we'll arbitrarily make the program stop running at some point" does not make "smart contracts" written in Ethereum "decidable" - as we've seen, these contracts can still blow up / go wrong in other ways before they run out of gas." https://www.reddit.com/r/btc/comments/4p0gq3/why_turingcomplete_smart_contracts_are_doomed/ https://www.reddit.com/r/btc/comments/4p0gq3/why_turingcompl...
- benchaney 9y ago
  This comment is simply incorrect. The gas limits do make smart contracts decidable. It is a mathematical fact. Bringing the idea that things have gone wrong with Ethereum as proof to the contrary is completely absurd. Things have also gone wrong with Bitcoin [1]. Is it undecidable now too? [1] https://en.wikipedia.org/wiki/Mt._Gox https://en.wikipedia.org/wiki/Mt._Gox
  - jude- 9y ago
    > This comment is simply incorrect. The gas limits do make smart contracts decidable. It is a mathematical fact. This line of reasoning does not help me write better code, and does not address the parent's concerns. Using this argument, I can say that every single program I will ever run in my lifetime is also decidable, since eventually the computer I'm using to run it will stop working. This of course does not mean that I will write bug-free code, nor does it mean that I will write code that is feasible to prove correct. What I want is a decidable programming language where it is always feasible to reason about the smart contract's halting states for arbitrary input. Bitcoin and its derivatives let me do this. Ethereum does not.
    - nicksdjohnson 9y ago
      Sure it does - the marvelous thing about a turing-complete virtual machine is that you can write a decidable language that compiles to EVM bytecode.
      - jude- 9y ago
        Sorry, I didn't qualify "always feasible" well enough. What I meant was, I want it to be feasible to reason about the halting states of every single smart-contract that will ever interact with my code. Not just the ones that I write, but also the ones that are reachable from my smart contract's call graph, and the ones that call into my smart contract. If I can do this, then I can feasibly reason about how my code will react to other peoples' inputs (e.g. I can prove the absence of DAO-like re-entrance bugs). The fact that Ethereum allows smart contracts to be written in undecidable languages means that this is not feasible in practice.
        nicksdjohnson 9y ago
        I don't think I follow - why would you need to reason about your callers' internal states in order to prove properties about your own contract?

MarkPNeyer 9y ago

To elaborate: You can look at some programs with your mind, and tell quite clearly what they'll do. You can't write a _program_ that will look at other programs, and always give a correct answer.

RichardHeart 9y ago

"The naïve Ethereum people think they've cleverly sidestepped this with the notion of "gas" but actually all they're doing is cheating with this messy kludge: because simply saying "we'll arbitrarily make the program stop running at some point" does not make "smart contracts" written in Ethereum "decidable" - as we've seen, these contracts can still blow up / go wrong in other ways before they run out of gas." https://www.reddit.com/r/btc/comments/4p0gq3/why_turingcomplete_smart_contracts_are_doomed/ https://www.reddit.com/r/btc/comments/4p0gq3/why_turingcompl...

benchaney 9y ago
This comment is simply incorrect. The gas limits do make smart contracts decidable. It is a mathematical fact. Bringing the idea that things have gone wrong with Ethereum as proof to the contrary is completely absurd. Things have also gone wrong with Bitcoin [1]. Is it undecidable now too? [1] https://en.wikipedia.org/wiki/Mt._Gox https://en.wikipedia.org/wiki/Mt._Gox
- jude- 9y ago
  > This comment is simply incorrect. The gas limits do make smart contracts decidable. It is a mathematical fact. This line of reasoning does not help me write better code, and does not address the parent's concerns. Using this argument, I can say that every single program I will ever run in my lifetime is also decidable, since eventually the computer I'm using to run it will stop working. This of course does not mean that I will write bug-free code, nor does it mean that I will write code that is feasible to prove correct. What I want is a decidable programming language where it is always feasible to reason about the smart contract's halting states for arbitrary input. Bitcoin and its derivatives let me do this. Ethereum does not.
  - nicksdjohnson 9y ago
    Sure it does - the marvelous thing about a turing-complete virtual machine is that you can write a decidable language that compiles to EVM bytecode.
    - jude- 9y ago
      Sorry, I didn't qualify "always feasible" well enough. What I meant was, I want it to be feasible to reason about the halting states of every single smart-contract that will ever interact with my code. Not just the ones that I write, but also the ones that are reachable from my smart contract's call graph, and the ones that call into my smart contract. If I can do this, then I can feasibly reason about how my code will react to other peoples' inputs (e.g. I can prove the absence of DAO-like re-entrance bugs). The fact that Ethereum allows smart contracts to be written in undecidable languages means that this is not feasible in practice.
      - nicksdjohnson 9y ago
        I don't think I follow - why would you need to reason about your callers' internal states in order to prove properties about your own contract?