4 ms·

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 probl

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.

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.