5 ms·

Turing-completeness was the entire conceit of Ethereum, as I understand it- without that you would have Bitcoin with a few bells and whistles, and no one would

Turing-completeness was the entire conceit of Ethereum, as I understand it- without that you would have Bitcoin with a few bells and whistles, and no one would bother. And once you're committed to that, a new language and environment are essential- something this entire fiasco shows is that a language for contract programming has very different requirements than what software engineers are currently used to, in order to be safe in ways that don't apply to ordinary software. In all likelihood, a working and reliable Ethereum simply requires computer science theories we don't have yet. A working Solidity would probably look something like Ada, but with types and invariants the likes of which we've never seen. Its potentially a very interesting research subject! But for now, yes, investing in Ethereum is like climbing aboard in a rocket aimed at Mars- exciting and futuristic, but unlikely to get you where you hope to go.

dvdkhlng 10y ago
I think we have a lot of theory about turing-complete computation. I really wonder why somebody would be willing to sign a turing-complete contract? The problem of understanding properties of the contract may be NP-hard [1] i.e. practicallly uncomputable. It may even be undecidable by involving instances of the halting problem [2]. [1] https://en.wikipedia.org/wiki/NP-hardness https://en.wikipedia.org/wiki/NP-hardness [2] https://en.wikipedia.org/wiki/Halting_problem https://en.wikipedia.org/wiki/Halting_problem
- danbruc 10y ago
  It is undecidable in the general case as shown by Rice's theorem [1]. [...] Rice's Theorem may essentially be generalized from Turing machines to most computer programming languages: there exists no automatic method that decides with generality non-trivial questions on the behavior of computer programs. [1] https://en.wikipedia.org/wiki/Rice%27s_theorem https://en.wikipedia.org/wiki/Rice%27s_theorem
  - mbrock 10y ago
    Of course, that doesn't mean you can't prove anything. It just means you can't prove things generally and automatically. For example, you can't solve the halting problem in general, but you can most definitely prove that a specific program terminates, or that large classes of programs all terminate. The proof of Rice's theorem boils down to the impossibility of the halting problem. The parent comment asks why someone would agree to a "Turing complete contract". But it's not necessary for an Ethereum contract to be "Turing complete" any more than Quicksort is "Turing complete". If the contract's code does something simple, we can verify and prove that it behaves as expected. It wouldn't be impossible to create a "safe" DAO-like contract.
    - dvdkhlng 10y ago
      But wouldn't Ethereum be a lot safer to use if its contract system would only have so many degrees of freedom, that all side effects and properties of contracts were computable for all contracts in a practical amount of time? With the current system I imagine one could even utilize homomorphic encryption to implement another Ethereum inside Ethereum that is cryptographically protected not only against modification but also against inspection :)
      - mbrock 10y ago
        I'd love to see an example of such a restricted contract language. My speculation is that we'll see a few different languages pop up with different approaches to safety, along with coding methodologies and tools for static analysis. Maybe we'll also discover a handful of primitive contract building blocks, to be implemented with care and stringency, with methods for combining them.
        naasking 10y ago
        > I'd love to see an example of such a restricted contract language. A Formal Language for Analyzing Contracts, http://szabo.best.vwh.net/contractlanguage.html http://szabo.best.vwh.net/contractlanguage.html Composing contracts: an adventure in nancial engineering, https://lexifi.com/files/resources/MLFiPaper.pdf https://lexifi.com/files/resources/MLFiPaper.pdf
- naasking 10y ago
  > The problem of understanding properties of the contract may be NP-hard [1] i.e. practicallly uncomputable. The difficulty makes good contract design a valuable service (like hiring lawyers). Otherwise everyone would just write their own contracts. A more declarative, less powerful language would have opened this up at the expense of contract succinctness.

dvdkhlng 10y ago

I think we have a lot of theory about turing-complete computation. I really wonder why somebody would be willing to sign a turing-complete contract? The problem of understanding properties of the contract may be NP-hard [1] i.e. practicallly uncomputable. It may even be undecidable by involving instances of the halting problem [2]. [1] https://en.wikipedia.org/wiki/NP-hardness https://en.wikipedia.org/wiki/NP-hardness [2] https://en.wikipedia.org/wiki/Halting_problem https://en.wikipedia.org/wiki/Halting_problem

danbruc 10y ago
It is undecidable in the general case as shown by Rice's theorem [1]. [...] Rice's Theorem may essentially be generalized from Turing machines to most computer programming languages: there exists no automatic method that decides with generality non-trivial questions on the behavior of computer programs. [1] https://en.wikipedia.org/wiki/Rice%27s_theorem https://en.wikipedia.org/wiki/Rice%27s_theorem
- mbrock 10y ago
  Of course, that doesn't mean you can't prove anything. It just means you can't prove things generally and automatically. For example, you can't solve the halting problem in general, but you can most definitely prove that a specific program terminates, or that large classes of programs all terminate. The proof of Rice's theorem boils down to the impossibility of the halting problem. The parent comment asks why someone would agree to a "Turing complete contract". But it's not necessary for an Ethereum contract to be "Turing complete" any more than Quicksort is "Turing complete". If the contract's code does something simple, we can verify and prove that it behaves as expected. It wouldn't be impossible to create a "safe" DAO-like contract.
  - dvdkhlng 10y ago
    But wouldn't Ethereum be a lot safer to use if its contract system would only have so many degrees of freedom, that all side effects and properties of contracts were computable for all contracts in a practical amount of time? With the current system I imagine one could even utilize homomorphic encryption to implement another Ethereum inside Ethereum that is cryptographically protected not only against modification but also against inspection :)
    - mbrock 10y ago
      I'd love to see an example of such a restricted contract language. My speculation is that we'll see a few different languages pop up with different approaches to safety, along with coding methodologies and tools for static analysis. Maybe we'll also discover a handful of primitive contract building blocks, to be implemented with care and stringency, with methods for combining them.
      - naasking 10y ago
        > I'd love to see an example of such a restricted contract language. A Formal Language for Analyzing Contracts, http://szabo.best.vwh.net/contractlanguage.html http://szabo.best.vwh.net/contractlanguage.html Composing contracts: an adventure in nancial engineering, https://lexifi.com/files/resources/MLFiPaper.pdf https://lexifi.com/files/resources/MLFiPaper.pdf
naasking 10y ago
> The problem of understanding properties of the contract may be NP-hard [1] i.e. practicallly uncomputable. The difficulty makes good contract design a valuable service (like hiring lawyers). Otherwise everyone would just write their own contracts. A more declarative, less powerful language would have opened this up at the expense of contract succinctness.