4 ms·

The problem with Turing completeness is that if it's not there from the start, people inevitably end up needing features that aren't present in the restricted l

The problem with Turing completeness is that if it's not there from the start, people inevitably end up needing features that aren't present in the restricted language, and then a Turing complete language is added to either the original system or a successor, and being an afterthought it usually ends up being a hack job. Examples: SQL was supplemented with procedural languages for stored procedures, Excel was supplemented with VBA, HTML was supplemented with JavaScript and, well, Bitcoin was supplemented with Ethereum. So providing a Turing complete language was the right decision as far as it goes, but it's not enough by itself. If you need reliability - which this does - it needs to be the case that typical code does not involves arbitrarily complex computation. Typical code needs to fit stereotyped patterns whose behavior is predictable. If Ethereum is to continue, it's clear that exhorting people to try even harder not to make mistakes in the current version of Solidity, won't cut it. The language needs to be supplemented or replaced with something that makes it easy to write correct code for the kind of things people typically want to do.

edejong 10y ago
There are languages which are both expressive and Turing incomplete, for example Coq. In the Coq language, Turing incompleteness is actually needed to be able to make complete proofs. Maybe Solidity would have been better implemented within Coq, but it's too late now.
- lmm 10y ago
  See http://publications.lib.chalmers.se/records/fulltext/234939/234939.pdf http://publications.lib.chalmers.se/records/fulltext/234939/... (suggesting Idris for this use case)
  - mbrock 10y ago
    That particular thesis actually ends up recommending against using a dependent functional language for Ethereum contracts... I think we might need to think of contracts as very important algorithms and prove them like we prove quick sort. That doesn't require dependent typing and functional programming; you can prove theorems about imperative code if you just have formal semantics. I'd be interested to see a verified dependently typed compiler to EVM for some simple language... but it kind of seems like a PhD project.
- lomnakkus 10y ago
  Edwin Brady's coined(?) a nice term for this: Pacman Complete
- rwallace 10y ago
  Is it too late now? It seems to me that it should be possible to implement a better language on top of the existing system, there are plenty of languages that compile to JavaScript after all, so it's still worth discussing what a better language might look like. You say Coq is expressive; okay, but in what sense, for what purposes? A language which isn't Turing complete - or even one which is - isn't going to be expressive for all purposes. As I understand it, Coq is designed to be expressive for the kind of things people doing research in type theory want to write, in the same way SQL is designed to be expressive for database queries. What sort of things do smart contracts typically want to say? Are they more similar to type theory research, database queries or something else? One possible answer is that it's too early to say yet, in which case perhaps extensibility is an important attribute. For example, suppose Racket were used as a language for writing smart contracts, with a backend to generate Ethereum byte code. Being a dialect of Lisp, Racket is highly extensible. It also has an optional type system. Do smart contracts tend to be prone to the kind of errors that are caught by a type system? If so, it would be worth using one.
  - mbrock 10y ago
    Note that Solidity is not JavaScript, it's just superficially similar in some ways. The comparison with JavaScript is for marketing pretty much. In particular, Solidity is statically typed. I would say that smart contracts are a lot like event processors that update bits of contract-local state and enforce preconditions. They are run in a single "thread" in blockchain order, but they can also invoke each other reentrantly (and that's the major source of confusion so far, so it should be limited and made very explicit). Some contracts perform more complex calculations, e.g. I know of one that calculates compound interest using fixed point math. There might be room for several different simpler languages for different purposes... It would make sense to use the most restricted language that can express the contract you want.
    - rwallace 10y ago
      From what I've seen of the discussion on this, you're right about uncontrolled reentrancy being a big source of problems. One thing that occurs to me: would the command-query distinction be a useful notion here? I have no truck with it in the general context in which it was coined, but in this context maybe it would be useful to draw a hard line distinction between 'I call you to ask for information' and 'I call you to ask for money'.
- jobigoud 10y ago
  > it's too late now Ethereum uses a virtual machine. There already have been several different languages to write contracts.
- cwmma 10y ago
  Coq is pretty specific in what it does like css (also Turing incomplete. There is a pretty low bar for features needed to make something Turing, it doesn't take much more then mutable variables and a while loop or recursive functions to impliment rule 110
  - kolinko 10y ago
    css3 is turning complete iirc
    - cwmma 10y ago
      you are thinking of this[1], it relies on a human following directions due to css not having any ability to calculate rules based on the results of other rules so if that was turning complete then by the same logic a piece of paper with instructions for how to do rule 110 would also be turing complete because a human could use that to calculate rule 110. 1. http://eli.fox-epste.in/rule110-full.html http://eli.fox-epste.in/rule110-full.html
- chriswarbo 10y ago
  Interestingly, Coq is expressive enough to write arbitrary computations; for example, you can write a Universal Turing Machine emulator; or, more realistically, many people write programming language implementations in Coq, in order to prove results about them. However, Coq can only run those computations for a given number of steps; in other words, you can't say "run this until it halts, and give me the result", but you can say "give me the result after 3^^^3 steps, or 'Nothing' if it hasn't halted by then". The reason this is interesting in this discussion is that Ethereum uses "gas" in a similar way.
- a-nikolaev 10y ago
  Yep, yep, and if contracts were written in Coq or a similar language, it would be easier to formally prove that they are "safe" from smarty pants hackers.. That would be a really nice application for formal methods, it seems.

edejong 10y ago

There are languages which are both expressive and Turing incomplete, for example Coq. In the Coq language, Turing incompleteness is actually needed to be able to make complete proofs. Maybe Solidity would have been better implemented within Coq, but it's too late now.

lmm 10y ago
See http://publications.lib.chalmers.se/records/fulltext/234939/234939.pdf http://publications.lib.chalmers.se/records/fulltext/234939/... (suggesting Idris for this use case)
- mbrock 10y ago
  That particular thesis actually ends up recommending against using a dependent functional language for Ethereum contracts... I think we might need to think of contracts as very important algorithms and prove them like we prove quick sort. That doesn't require dependent typing and functional programming; you can prove theorems about imperative code if you just have formal semantics. I'd be interested to see a verified dependently typed compiler to EVM for some simple language... but it kind of seems like a PhD project.
lomnakkus 10y ago
Edwin Brady's coined(?) a nice term for this: Pacman Complete
rwallace 10y ago
Is it too late now? It seems to me that it should be possible to implement a better language on top of the existing system, there are plenty of languages that compile to JavaScript after all, so it's still worth discussing what a better language might look like. You say Coq is expressive; okay, but in what sense, for what purposes? A language which isn't Turing complete - or even one which is - isn't going to be expressive for all purposes. As I understand it, Coq is designed to be expressive for the kind of things people doing research in type theory want to write, in the same way SQL is designed to be expressive for database queries. What sort of things do smart contracts typically want to say? Are they more similar to type theory research, database queries or something else? One possible answer is that it's too early to say yet, in which case perhaps extensibility is an important attribute. For example, suppose Racket were used as a language for writing smart contracts, with a backend to generate Ethereum byte code. Being a dialect of Lisp, Racket is highly extensible. It also has an optional type system. Do smart contracts tend to be prone to the kind of errors that are caught by a type system? If so, it would be worth using one.
- mbrock 10y ago
  Note that Solidity is not JavaScript, it's just superficially similar in some ways. The comparison with JavaScript is for marketing pretty much. In particular, Solidity is statically typed. I would say that smart contracts are a lot like event processors that update bits of contract-local state and enforce preconditions. They are run in a single "thread" in blockchain order, but they can also invoke each other reentrantly (and that's the major source of confusion so far, so it should be limited and made very explicit). Some contracts perform more complex calculations, e.g. I know of one that calculates compound interest using fixed point math. There might be room for several different simpler languages for different purposes... It would make sense to use the most restricted language that can express the contract you want.
  - rwallace 10y ago
    From what I've seen of the discussion on this, you're right about uncontrolled reentrancy being a big source of problems. One thing that occurs to me: would the command-query distinction be a useful notion here? I have no truck with it in the general context in which it was coined, but in this context maybe it would be useful to draw a hard line distinction between 'I call you to ask for information' and 'I call you to ask for money'.
jobigoud 10y ago
> it's too late now Ethereum uses a virtual machine. There already have been several different languages to write contracts.
cwmma 10y ago
Coq is pretty specific in what it does like css (also Turing incomplete. There is a pretty low bar for features needed to make something Turing, it doesn't take much more then mutable variables and a while loop or recursive functions to impliment rule 110
- kolinko 10y ago
  css3 is turning complete iirc
  - cwmma 10y ago
    you are thinking of this[1], it relies on a human following directions due to css not having any ability to calculate rules based on the results of other rules so if that was turning complete then by the same logic a piece of paper with instructions for how to do rule 110 would also be turing complete because a human could use that to calculate rule 110. 1. http://eli.fox-epste.in/rule110-full.html http://eli.fox-epste.in/rule110-full.html
chriswarbo 10y ago
Interestingly, Coq is expressive enough to write arbitrary computations; for example, you can write a Universal Turing Machine emulator; or, more realistically, many people write programming language implementations in Coq, in order to prove results about them. However, Coq can only run those computations for a given number of steps; in other words, you can't say "run this until it halts, and give me the result", but you can say "give me the result after 3^^^3 steps, or 'Nothing' if it hasn't halted by then". The reason this is interesting in this discussion is that Ethereum uses "gas" in a similar way.
a-nikolaev 10y ago
Yep, yep, and if contracts were written in Coq or a similar language, it would be easier to formally prove that they are "safe" from smarty pants hackers.. That would be a really nice application for formal methods, it seems.