4 ms·

As I understand it: It's true of any platform, but Etherium is at a far higher risk of getting hacked because the language is Turing complete. There could conc

As I understand it: It's true of any platform, but Etherium is at a far higher risk of getting hacked because the language is Turing complete. There could conceivably be a smart contract blockchain with a simplified language that was still capable of most of Etherium's good sides with the safety net of static verification tools.

heliumcraft 10y ago
ALL general purpose programming languages (C++, Java, etc..) are Turing Complete and this is an essential feature for creating decentralised applications (or any software really).
- PeCaN 10y ago
  Um, no, that's just factually incorrect. You can do very, very many useful things without Turing completeness. You cannot be fully general, but there's active research on how far you can get. Restricted subsets of query languages like SQL and Datalog are perhaps the most common (though more or all SQL implementations are Turing complete) and indeed quite useful. I can easily imagine a system built on a non-Turing complete logical query language that defines data and rules for presentation. You could get pretty far with that. You can't create _any_ application, but calling Turing completeness “essential … for decentralized applications” is incorrect. It's essential for a _subset_ of applications that require Turing completeness. I've been saying ETH is broken for a while. Its computational ability means contracts _cannot_ be formally verified. This is why I didn't buy into the DAO, and sure enough there's a bug in the DAO (ironically recursion related).
  - pron 10y ago
    People are under the impression that not being Turing complete is somehow enough to be feasibly verifiable. If we place (realizable) computational models on a scale, with 0 being no computation at all, and 10 being Turing completeness, then the computational models we can generally verify are somewhere between 0 and 1 (with 1 being, say, FSMs). A language with no loops, no recursion and just subroutines and binary variables -- i.e. it's an FSM -- is already PSPACE-complete to verify, meaning we can only verify only very short programs in that language. In other words, you need to get very far from Turing completeness to be generally verifiable. This is why in general software verification doesn't try to come up with languages where all programs are verifiable, but aims to verify specific programs, sometimes regardless of the computational strength. Some programs in Turing complete languages can be verified (but certainly not all), just as some programs in FSM-strength languages can be verified (but certainly not all). While it is certainly possible that a much bigger subset of, say, FSM programs can be verified than a subset of programs in TC languages, placing the bar at "Turing complete" is somewhat of a red herring. Indeed, the LANGSEC link in the post[1] seems to understand that, noting that even verifying PDAs is undecidable, but it fails to note that even decidable verification tasks (for FSMs) are very often intractable, which -- for all practical purposes -- is just as bad as being undecidable. [1]: http://langsec.org/occupy/ http://langsec.org/occupy/
j1vms 10y ago
> It's true of any platform, but Etherium is at a far higher risk of getting hacked because the language is Turing complete. Ethereum, the VM/system is Turing complete, but Ethereum of course is not a language itself. [Correction: EVM code, that is Ethereum VM assembly, is indeed a language. Thus, Ethereum is technically both a VM and a language ("EVM assembly code") - which makes the assertion that "Ethereum is a language" correct after all.] As far as I understand it, all current Ethereum languages (e.g. Solidity) are also Turing complete, though it should be possible to create a language for Ethereum to produce only algorithms constrained with some level of decidability. This is why Ethereum is likely not doomed yet as some have claimed recently. However, and especially due to The DAO fiasco, it's now a matter of building static verification tools as you suggest, or decidable languages for it, and new cryptosystems may show up before it can get to its first killer app. Full disclosure: No horses in this race at the moment. As an aside, I think that everyone posting anything about Bitcoin or Ethereum should be posting a disclosure in each discussion (even an abridged one of some sort, just a couple of characters).

heliumcraft 10y ago

ALL general purpose programming languages (C++, Java, etc..) are Turing Complete and this is an essential feature for creating decentralised applications (or any software really).

PeCaN 10y ago
Um, no, that's just factually incorrect. You can do very, very many useful things without Turing completeness. You cannot be fully general, but there's active research on how far you can get. Restricted subsets of query languages like SQL and Datalog are perhaps the most common (though more or all SQL implementations are Turing complete) and indeed quite useful. I can easily imagine a system built on a non-Turing complete logical query language that defines data and rules for presentation. You could get pretty far with that. You can't create _any_ application, but calling Turing completeness “essential … for decentralized applications” is incorrect. It's essential for a _subset_ of applications that require Turing completeness. I've been saying ETH is broken for a while. Its computational ability means contracts _cannot_ be formally verified. This is why I didn't buy into the DAO, and sure enough there's a bug in the DAO (ironically recursion related).
- pron 10y ago
  People are under the impression that not being Turing complete is somehow enough to be feasibly verifiable. If we place (realizable) computational models on a scale, with 0 being no computation at all, and 10 being Turing completeness, then the computational models we can generally verify are somewhere between 0 and 1 (with 1 being, say, FSMs). A language with no loops, no recursion and just subroutines and binary variables -- i.e. it's an FSM -- is already PSPACE-complete to verify, meaning we can only verify only very short programs in that language. In other words, you need to get very far from Turing completeness to be generally verifiable. This is why in general software verification doesn't try to come up with languages where all programs are verifiable, but aims to verify specific programs, sometimes regardless of the computational strength. Some programs in Turing complete languages can be verified (but certainly not all), just as some programs in FSM-strength languages can be verified (but certainly not all). While it is certainly possible that a much bigger subset of, say, FSM programs can be verified than a subset of programs in TC languages, placing the bar at "Turing complete" is somewhat of a red herring. Indeed, the LANGSEC link in the post[1] seems to understand that, noting that even verifying PDAs is undecidable, but it fails to note that even decidable verification tasks (for FSMs) are very often intractable, which -- for all practical purposes -- is just as bad as being undecidable. [1]: http://langsec.org/occupy/ http://langsec.org/occupy/

j1vms 10y ago

> It's true of any platform, but Etherium is at a far higher risk of getting hacked because the language is Turing complete. Ethereum, the VM/system is Turing complete, but Ethereum of course is not a language itself. [Correction: EVM code, that is Ethereum VM assembly, is indeed a language. Thus, Ethereum is technically both a VM and a language ("EVM assembly code") - which makes the assertion that "Ethereum is a language" correct after all.] As far as I understand it, all current Ethereum languages (e.g. Solidity) are also Turing complete, though it should be possible to create a language for Ethereum to produce only algorithms constrained with some level of decidability. This is why Ethereum is likely not doomed yet as some have claimed recently. However, and especially due to The DAO fiasco, it's now a matter of building static verification tools as you suggest, or decidable languages for it, and new cryptosystems may show up before it can get to its first killer app. Full disclosure: No horses in this race at the moment. As an aside, I think that everyone posting anything about Bitcoin or Ethereum should be posting a disclosure in each discussion (even an abridged one of some sort, just a couple of characters).