Money is a social technology that solves a social problem. Cryptocurrency is a engineering technology in search of a problem to solve.
Do you mean on the margin where there is debate about the contract or whether the goods/services were rendered adequately?
Cryptocurrencies don't attempt to solve this problem at all, they simply allow for efficient moving of currency between parties without the need for meatspace regulation/trust to do it.
Smart contracts make sense with a blockchain because now humans can agree on specific contract behavior that is fixed due to the highly prescribed way a VM will process it. This doesn't mean that humans will or should blindly trust a smart contract to do what some third party claims it will do.
But unlike meatspace, there is one VM that matters, contracts and oracles can earn a reputation as being trustworthy, and established patterns can be executed with incredible efficiency and fairness.
The issue that presents a challenge for all systems (cryptocurrencies and meatspace institutions) is bootstrapping. Some people will get burned in the beginning because fraud will be temporarily easier to commit. This is why I wish the DAO had just been allowed to die without the hard fork. What is needed is not innovative crowd funding schemes, but additional trust and vetting infrastructure.
Btc isn't here to pay your coffee or your salary, it's here as a fallback if you really need to get out of traditional finance. Same with ETH. You're not supposed to switch all your banking, notarial or legal affairs to the platform but it's there for cases where traditional contract law isn't desirable.
Now why so many people ascribed additional meaning or value to these platforms is the really interesting part. In a way, it's good these hacks happen as a reminder that this is what you signed up for. It's the wild west and you don't have a court or government watching your back. That's a (the) feature.
Unexpected downsides for whom? Smart contracts cease to be smart if we have to rely not on the VM but on a small group of human overlords.
If a smart contract exists and you don't know clearly how many times it has been used and what percentage of the parties who used it are pleased with its functioning, you really should not use it unless you feel comfortable personally reviewing the code.
With the insane decision to use a Turing-complete language, the contract's behavior undecidable. You don't even know if the contract will halt.
Limited "gas" (execution time) isn't the solution, because the lesson of the Halting Problem isn't that a program might not terminate. Even if the program halts within a finite time (or "gas"), the behavior of the program on the current input is still undecidable.
Any serious attempt at writing "smart contracts" should demonstrate their understanding of the science of insecurity[1] and limit the contract language's complexity to deterministic context-free.
[1] https://media.ccc.de/v/28c3-4763-en-the_science_of_insecurit...
If were really that bad to use Turing-complete code, then smart contracts would be the least of our problems, because Turing-complete code runs our airplanes, medical equipment, and nuclear reactors.
Ethereum programs aren't Turing complete. They always halt. Turing complete programs don't generally halt. That's the definition.
You should demonstrate your understanding by using these terms correctly!
This whole argument about Turing completeness is a huge red herring.
The Parity multisig attack was an extremely simple programming error that has nothing to do with Turing completeness.
That people put their trust in such a contract despite its source code being obviously wrong points to the real problem.
The real problem right now is the lack of convenient tools and established practices for formal verification. If you think formal verification is impossible for EVM, you're wrong and you fundamentally misunderstand computation.
I've seen this criticism over and over again on internet forums: "EVM is so stupid, it can't be formally verified because it's Turing complete."
It's totally wrong: EVM isn't Turing complete, and it doesn't matter.
Look at "The Art of Computer Programming." It's full of Knuth's proofs of the correctness of algorithms written in assembler and imperative code. Look at any proof of correctness of a sorting algorithm.
OBVIOUSLY you can prove the correctness of programs written in Turing complete languages. You just look at the specification of the language, formulate a specification of your program's intended behavior, and then prove that the code matches the specification. This is how formal verification works, regardless of Turing-completeness.
To clarify, what is the impact of Turing completeness on formal verification? It means that for some ARBITRARY program, you cannot ALWAYS prove that it halts.
But even with some non-Turing complete formalism, you obviously cannot automatically prove the correctness of an arbitrary program; that's just nonsense. You could be certain that the program halts, sure, but how valuable is that? Ethereum already guarantees that all programs halt using the very simple gas mechanism.
Did you actually read my post? I'm not claiming halting is a problem; it's merely an example of undecidability. The "gas limit" doesn't help in the cases where the program does halt with unexpected behavior.
> Turing complete programs don't generally halt. That's the definition.
Where did you get this nonsense? See [1] for the actual definition.
> attack was an extremely simple programming error
Yes, which is why it's stupid to use a language with a grammar that cannot be proven. If trivial mistakes happened in production code, how do you expect to find the subtle bugs that happen because of the complex interactions that occur in recursively enumerable grammars?
> prove the correctness of programs
You can do that for some programs, but not all. The point about grammars is there are classes of grammar that allow automatic verification. Using a recursively enumerable grammar instead of a regular or context-free grammar demonstrates a severe misunderstanding of either language theory, or secure/safe engineering practices.
int_19h description[2] of some of the insane parts of Solidity suggests a PHP-style fractal of bad design[3], not a platform for proving correctness.
[1] https://en.wikipedia.org/wiki/Turing_completeness#Formal_def...
[2] https://news.ycombinator.com/item?id=14810008
[3] https://eev.ee/blog/2012/04/09/php-a-fractal-of-bad-design/
Here's how reasonable Ethereum contract development should happen. You construct the contract, either in some high level language or in bytecode. Then you prove, using some reasonable formalism (TLA+, Isabelle, paper, symbolic execution, or whatever), that the contract does what it should do. Then people who want to trust the contract look at this proof.
This is not at all hindered by the EVM being quasi Turing complete, because at no point do you have the question "How can I mechanically verify halting of an arbitrary program?"
OTOH, if the language isn't Turing-complete, there will almost certainly be things you'll want a contract to do that it can't. You can have generality or decidability, but not both.
Based on other comments here there certainly may be questionable decisions in the design of Solidity but that doesn't mean Turing-completeness is one of them.
The idea that we will ever stop needing human arbiters is laughable and pure hubris.
Maybe if the contracts had more constrained semantics ETH programming would be less scary, at the cost of some bells and whistles or more verbose syntax.
It is possible to have trusted contracts, iff their logic is (mathematically) proven. But the VM can't make contracts more secure by itself.
Being Turing-complete means it's possible to write some contracts/programs for which certain features are undecidable by analysis.
It doesn't mean that programs that could be also be written in any more limited language can't have all the properties about then that could be proven in the non-Turing complete language proven when written in the Turing-complete language.
> It is possible to have trusted contracts, iff their logic is (mathematically) proven.
Trustworthiness of programs (including “smart contracts”, which are only loosely analogous to traditional contracts) is about whether the actual people using them get what they expect out of their behavior. Mathematical proofs of formal properties may be useful to that in some cases, but are not generally sufficient.
Suppose a non-Turing-complete language were used instead. Now, imagine a contract that is highly complex. If a layperson decides to trust that contract without reading the code, does it matter whether the language used to implement the contract was Turing-complete or not?
I'd argue that trust of contracts is pragmatically more of a social concept than a computational concept, since at scale the vast majority of contract users would make their trust decision about a contract based on non-technical factors.
Um, yes? Literally the point of weaker languages in this context is that they can be statically provable.
Arguably unclear termination semantics would be a good reason not to trust a contract. Ideally trust mechanisms would exist such that closed source contracts were trustable via a pure insurance-based mechanism.
As I attempted to say in my previous comment, undecidability[1] isn't limited to deciding if a program will halt (or even the weaker question of if it will halt in a given finite time). Recursively enumerable[2] languages that require a Turing machine to automate have an intrinsic complexity (i.e. any Turing-complete language). This isn't a "work harder to solve it" level of complexity; some behavior will always be undecidable.
You might experience this problem in the traditional form of the "Halting Problem" where the question "Will this program halt?" may be answered with "I don't know, it's still running" in addition to "yes" or "no". However, this level of complexity can also cause unexpected output due to subtle interactions inside the program that are difficult to predict from the source. Some behaviors are provably unknowable.
You can avoid this problem by using a simpler class of language. Regular languages (which "regular expression" match[3]) are safe, as are deterministic context-free[4] languages. You may find the lack of loops limiting.
[1] https://en.wikipedia.org/wiki/Undecidable_problem
[2] https://en.wikipedia.org/wiki/Chomsky_hierarchy#Type-0_gramm...
[3] basic regexp, not PCRE or other language-sepcific extensions!
[4] https://en.wikipedia.org/wiki/Context-free_grammar#Undecidab...
What if Ethereum offered a non-turning-complete subset of Solidity (that included formal verification) which could optionally be used in smart contracts. Would this cause you to view the platform differently?