4 ms·

Actually, we kind of discovered that, unless we radically cripple our model (eg. by removing the first-class-citizen property) Turing-completeness is basically

Actually, we kind of discovered that, unless we radically cripple our model (eg. by removing the first-class-citizen property) Turing-completeness is basically irrelevant either way. https://github.com/ethereum/wiki/wiki/Whitepaper-2-Draft#computation-and-turing-completeness https://github.com/ethereum/wiki/wiki/Whitepaper-2-Draft#com... I basically just chose to keep it in there because it makes a few contract types easier.

maaku 13y ago
Vitalik, are you aware of the construct of total functional programming languages? It is possible to have recursion without giving up solution to the halting problem.
- vbuterin 13y ago
  Pure functional programming? Yeah. But those aren't magic. Whenever you have conditional branching, the halting problem reintroduces itself. (def (collatz-depth x) (if (= x 1) 0 (if (= (mod x 2) 0) (+ 1 (collatz-depth (/ x 2))) (+ 1 (collatz-depth (+ 1 (* x 3))))))) is intractable no matter what language you use to write it in.
  - steveklabnik 13y ago
    Total functional programming is different than purely functional programming: http://en.wikipedia.org/wiki/Total_functional_programming http://en.wikipedia.org/wiki/Total_functional_programming
    - vbuterin 13y ago
      Ah okay, interesting, thanks for the link. So it's basically a maximally powerful non-Turing-complete language. I would argue that the section in our v2 whitepaper on non-Turing-complete languages still covers the fallacy behind that: you can still have exponential blowup, so you still need a concept of maximum steps, but then once you have a concept of maximum steps there's little benefit to restricting the programming language.
  - emn13 13y ago
    In essence, it's just recursion that's only allowed when the recursive input is in some sense strictly "smaller" than its input and therefore necessarily terminates if the input is of finite size and cannot drop below zero. However, it's not magic: it's not automatically trivial to generate such a proof of termination (I'd assume there exist definitely terminating programs for any given proof system that cannot be proven to terminate in that formalism), and it may be a moot point since a slow enough algorithm is for all intents and purposes non-terminating...

maaku 13y ago

Vitalik, are you aware of the construct of total functional programming languages? It is possible to have recursion without giving up solution to the halting problem.

vbuterin 13y ago
Pure functional programming? Yeah. But those aren't magic. Whenever you have conditional branching, the halting problem reintroduces itself. (def (collatz-depth x) (if (= x 1) 0 (if (= (mod x 2) 0) (+ 1 (collatz-depth (/ x 2))) (+ 1 (collatz-depth (+ 1 (* x 3))))))) is intractable no matter what language you use to write it in.
- steveklabnik 13y ago
  Total functional programming is different than purely functional programming: http://en.wikipedia.org/wiki/Total_functional_programming http://en.wikipedia.org/wiki/Total_functional_programming
  - vbuterin 13y ago
    Ah okay, interesting, thanks for the link. So it's basically a maximally powerful non-Turing-complete language. I would argue that the section in our v2 whitepaper on non-Turing-complete languages still covers the fallacy behind that: you can still have exponential blowup, so you still need a concept of maximum steps, but then once you have a concept of maximum steps there's little benefit to restricting the programming language.
- emn13 13y ago
  In essence, it's just recursion that's only allowed when the recursive input is in some sense strictly "smaller" than its input and therefore necessarily terminates if the input is of finite size and cannot drop below zero. However, it's not magic: it's not automatically trivial to generate such a proof of termination (I'd assume there exist definitely terminating programs for any given proof system that cannot be proven to terminate in that formalism), and it may be a moot point since a slow enough algorithm is for all intents and purposes non-terminating...