Personal attacks, which this crosses into, are not ok on Hacker News. Please edit such stuff out of your comments here.
We detached this subthread from https://news.ycombinator.com/item?id=11928562 and marked it off-topic.
I guess I felt the need to accuse someone as I felt frustrated. News like this really smears not only cryptocurrencies but software engineering in general. A single typo cost these people $50M is what they claim, but the reality is that the whole system was recklessly engineered. I guess I'm also saddened that so much money was put behind something that was so clearly recklessly engineered.
Would it been a crazy idea just to invest a million or two of the $250M to pay a Formal Methods team at any university in the world to give the language a quick do-over?
If it was phrased as "person XYZ is an asshole!" then I would agree that it's a personal attack.
Those are currently not the issues that require attention.
You can make it as fast and as large as you want, if it is broken at the root that's all pointless. First walk, then run. I'd be more impressed with a much smaller system without sharding and massive scaling properties if it was bullet proof.
Ethereum itself is more bullet proof, as there are multiple implementations and the description of the protocol better defined and has proofs inside.
That's the whole problem in a nutshell. I highly doubt that is the road to a viable solution but I'm patient enough to be proven wrong in the longer term. But anything that is Turing complete automatically implies that anything layered on top of it will incorporate such niceties as being impossible to formally verify due to the halting problem.
In other words: the only way to establish whether or not the code will try anything funny is to run it.
Whenever you want any guarantees about anything you implement a very restricted[1] subset of what a TM can do... at least if you're allowing users to input arbirtrary programs[2]. If you don't restrict to a non-TC language... you're -- in so many words -- fucked. (Hence the "hack".)
[1] Preferably using a statically typed PL, for obvious reasons. There's actually a thing these days where non-TC languages can actually "do things". My favorite moniker for this is "pacman-complete" (coined by Edwin Brady, I believe.)
[2] Having looked at a few .sol files earlier, they at least look TC, having general recursion and all.
Not sure I follow here... You can certainly run a non-turing-complete language on top of a turing-complete one and anything in that language could potentially be verifiable.
Edit: apparently the thefts so far are "only" 45 million.
Just kidding; bad joke; I just couldn't resist.
This is what happens when one does not do that. :)
I wouldn't be so hard on the kid. Now, the due diligence that should have been performed by the corporations that sank millions in to this project, who actually do hire plenty of people who are well educated and should have known better is another matter.
But I suppose jumping in early in to the tulip craze and riding it for all its worth is more important than taking the time and effort to make sure the system is reliable and robust before it goes live.
In addition to typesafety, it would have to be both explicitly typed at the lowest possible granularity and annotated with pre and post conditions.
Not only did this code allow a bunch of tokens be transferred without compensation, it left the whole accounting system in a corrupted state! One that could have easily been detected and verified at any point.
This line:
Should have looked like this: And the whole function 'splitDao' should have a type annotation that completely captures the possible actions it might encompass, and pre- and postconditions that at the very least constrain the result of the function to not corrupt the accounting of the DAO (i.e. it should still have as many tokens as it believes it has).It's nice that Vitalik Buterin is a genius, but it shows that this guy is only 22 and dropped out of university because anyone with a degree in computer science knows about this stuff and its importance in high reliability systems. He should have known the contract language should have had typechecked side effect and he should have known proper pre- postconditions would have been the least he should have done.