1. Ethereum is difficult to work with
2. Its difficulty does not provide security
This doesn't exactly inspire confidence in it.
Some comments on this article imply that this was just a scam, so maybe Ethereum is secure. I think that a lot of people learn about things they don't care about via headlines, which may be damaging for Ethereum in its infancy.
A fundamental principle of Ethereum is that its smart contracts have Turing-complete computing power. Therefore, there is no possibility of 'higher level abstractions' that will permit only legitimate contracts to be written (even if the abstractions are limited in their power, an attacker can make use of the full power of the underlying system.)
Writing provably-secure smart contracts is as difficult as writing provably-secure software for any other Turing-complete platform: i.e. only a small percentage of developers can do it. Furthermore, the software that comprises the platform itself has not been stringently verified.
Of course, we are using lots of software in banking and finance that is not formally verified, but there are significant differences: it runs in secured environments with controlled and very limited external access, and there are out-of-band methods for correcting mistakes. In contrast, blockchain currencies are actually promoted as being immune to this sort of interference on account of transactions being irrevokable (and no, the hard fork that rescued the DAO participants is not a counter-example, as that will not be feasible in future.)
I cannot say these problems will not be resolved in the future, but why would anyone put any significant value at risk until they are?
Your closing questions has a point I agree on.
High level abstractions and Turing completeness are not in opposition. Haskell, for example, offers high level abstractions in the form of a functional language with abstract data types, strong typing and purity (unless you specify something else explicitly, functions only have access to their arguments).
I think Safe Haskell would be a good Turing-complete, general purpose contract language. Untrusted code can be compiled to machine code and executed safely, by using a restricted IO monad that only allows specific input/output operations[1], so the contract logic can be executed safely without a sandbox.
[1] https://downloads.haskell.org/~ghc/7.4.1/docs/html/users_gui...
> there is no possibility of 'higher level abstractions' that will permit only legitimate contracts to be written
True, but there is the possibility of trivial changes that would prohibit some exceptionally catastrophic bugs. The language features that allowed last weeks multisig walled bug (delegation to an unknown function, public initialization code, the possibility of calling initialization code after initialization) need not be like that. A much better language could still be Turing complete but exclude such things (forcing you to write explicit code that shoots you in the foot, if you so wish).
Well, I didn't suggest it - it seems you are inventing that notion because you are obliged to agree with everything I actually wrote.
The point is not the relative safety of one language against another, but whether, in absolute terms, Ethereum will become safe enough for the sort of wide-ranging uses that its promoters envisage. If the sort of examples you present here are sufficient for that, then, given that security and correctness have been prized for long before Ethereum, one has to wonder why they have not already been used to create languages that are already secure and bug-resistant enough for Ethereum.
There is certainly some basic changes that could make Ethereum more secure, but past experience in this field suggests there is a whole range of hills beyond this one. And in security matters, going part-way is not much of an advance at all; such defenses can, like the Maginot line, be outflanked.
You wrote: "Writing provably-secure smart contracts is as difficult as writing provably-secure software for any other Turing-complete platform". This is not true. Writing provably-secure smart contracts in something like C would be strictly harder than in Solidity because there are more classes of possible errors, and hence more properties to be proved. There are meaningful differences in the ease of proof even among Turing-complete languages. And some things you would have to prove explicitly for programs in one language are automagically "proved" for you by other languages' compilers.
So yes, you did suggest that any two Turing-complete languages are equally safe and secure.
> because you are obliged to agree with everything I actually wrote
Haha. No.
What?
Wouldn't "choose one of these 10 contracts which have been proven correct, and also choose the parameter for said contract" be using a higher level abstraction?
And if the 10 contract are proven correct+secure, then this would be secure, right?
I don't understand what you meant by "an attacker can make use of the full power of the underlying system" such that it is compatible with the security of the abstraction I described.
To expand on point 1, given that your technique should be generally applicable, why has it not taken over all the other applications of computing where security and correctness matter? The reason, I believe, is that it is, in practice, infeasible for many of the sort of things that are useful and that we actually want to do.
I believe that people have made formally verified (trivial?) contracts (based on the spec of the vm iirc? Not sure), but I don't remember anything about a formally verified contract being used in practice. People definitely are making progress on the formal verification front (building foundations/infrastructure/etc.) but they aren't really there yet. ("There" being, ready for widespread use, and in widespread use)
I don't really understand why people buy into many of these ICOs. I mean, I'm somewhat enthusiastic about "smart contracts", but I don't actually own any cryptocurrency.
I don't mean to say that I think all ICOs are bad, but given the number that are failing, I find it hard to imagine that the people buying into them are doing enough research into them before buying for it to make sense.
Also, I don't understand why people aren't building contracts on top of a contract layer that handles arbitration for reversing fraudulent transactions yet? I thought that would have been built by now.
> Also, I don't understand why people aren't building contracts on top of a contract layer that handles arbitration for reversing fraudulent transactions yet? I thought that would have been built by now.
Ittay Eyal and Emin Gün Sirer have suggested at least a partial solution along those lines. I believe there is some opposition from those who consider the inviolability of transactions to be a non-negotiable feature of crypto currencies, as arbitration implies arbitrators, but this might be part of the future of smart contracts.
http://hackingdistributed.com/2016/07/11/decentralized-escap...
Your clarifications make sense though.
Oh please, a lot of people keep saying this, but the reality is that Ethereum and Solidity devs simply didn't do enough research. There's a long history of smart contract platforms that are both safer and more robust, and the problems inherent to the choices Solidity made were obvious right when it was first introduced:
FUD.
What are you talking about? Solidity is not so unsafe, nor is it correct to imply that Vitalik "didn't do his research". MAYBE he did his research and came to a different conclusion? Maybe hhis priorities were different? Regardless, he's exceptionally bright and by no measure just a hasty dev trying to make a quick buck.
And your link does not point to any inherent flaws in Solidity, just opinions on language fit.
Ethereum development IS in it's infancy. It WILL improve over time - like it or not.
What we're talking about are a slew of successful attacks in the ETH ecosystem. What we're talking about are what appear to be questionable decisions in Solidity. What do you think of this thread earlier? https://news.ycombinator.com/item?id=14810008
It is clearly unsafe, judging from these attacks. It is clearly not designed with security in mind, which should have been a top priority. "Maybe his priorities were different" is even more damning than if people did prioritize security and failed.
You say "clearly unsafe" but there has been, to my knowledge, only one serious flaw identified, and that is what lead to the fork. Many of these ICO thefts have been suspected internal jobs, not as the result of a new vulnerability identified.
correct me if i'm wrong. If ETH is doomed, i'm happy to let best of breed win. But I'm not seeing an argument made with facts here - I'm seeing Fear, Uncertainty, and Doubt.
I suggest you read the links in that thread that talk about the requirements of REAL smart contracts, and then come back and tell me Solidity is not hopelessly flawed.
As a language for writing smart contracts, Solidity is a total minefield of unsafety.
As for the reasonableness of "different conclusions", if Vitalik was responsible for Solidity, then I can't disagree more with everything you've said.
This seems small, and thus less trustworthy as a resource for me. Akin to a post on reddit with 10 upvotes and a handful of comments. I'm going to need to see more than that before I start taking those concerns seriously.
If it's obviously flawed, I'd expect more dialog and drum beating outside of one thread and among a larger group of people. I am not seeing that, presently.
There is a difference between the theory of programming, and actual programming. One is a science, the other involves a good deal of engineering and creativity. So while at a theoretical level there are concerns - it does not absolve engineering from addressing them. It is for this reason (and many more) that I do not take a forum post with a few replies as authoritative, on a forum i've never even heard of.
If you can't provide additional resources, thats fine. But lets be clear: i'm not interested in a pissing match. I'm trying to understand. I am yet to see anything yet that gives me pause surrounding ethereum smart contracts, aside from things I've already held concerns over (like the revocability issue) but which do not represent showstoppers for me.
Heck, buffer overflow bugs are decades old but still happen all the time.
Software security has practically not gotten any better over the years. Best practices are now known but rarely followed. Even when you follow best practices, there are vulnerabilities. Software security is an illusion.