5 ms·
In addition to this the language is not explicit enough. Even standard Haskell wouldn't be safe enough for a program that manages $250MM directly without safe g
by tinco 10y ago
In addition to this the language is not explicit enough. Even standard Haskell wouldn't be safe enough for a program that manages $250MM directly without safe guards.
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:
```
Transfer(msg.sender, 0, balances[msg.sender]);
```
Should have looked like this:
```
// postcondition: balances[msg.sender] == 0
Transfer(msg.sender, 0, balances[msg.sender]) :: Action<Transfer>;
// Compiler result:
// # Error 1: line XX expected type Action<Transfer> but instead got type Transfer
// # Error 2: line XX violates postcondition, expected balances[msg.sender] == 0, got balances[msg.sender] != 0
```
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.
- tmalsburg2 10y agoOne solution might be to design a safe language that compiles to the the language used in Ethereum. Not sure if possible within the given constraints.
- eudox 10y agoThe problem then becomes ensuring that only code compiled from that language can run.
- tmalsburg2 10y agoJust let people use whatever they want. Those who write unsafe contracts will get bitten but that's ok.
- krapp 10y agoWouldn't it be better to just rewrite everything in that safe language and abandon whatever Ethereum is written in?
- tmalsburg2 10y agoSure, but many people are so deeply invested in Etherum that I doubt that it's going to happen. But perhaps there will be a competing system.
- whazor 10y agoTo counter your attack on Buterin, he is aware that writing safe contract code requires proofs and type safety. That is why solidity is compiled to EVM code, so that improved languages could incorporate this. Solidity is built for rapid innovation and user friendliness. Buterin is now more busy with sharding and scaling issues.
- powera 10y agoPeople did lose $200 million dollars. Why is he focusing on scaling? Edit: apparently the thefts so far are "only" 45 million.
- marvy 10y agoSo that they can lose $2 billion instead :) Just kidding; bad joke; I just couldn't resist.
- jsprogrammer 10y agoI thought only a fifth of ~$115 million has been sequestered (apparently the action will be rolled back)?
- jacquesm 10y ago> Buterin is now more busy with sharding and scaling issues. 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.
- whazor 10y agoEthereum is a turing machine that runs code, programming languages are more high level. Creating an ADA-like language is trivial compared to making a scalable blockchain that supports computation. Ethereum itself is more bullet proof, as there are multiple implementations and the description of the protocol better defined and has proofs inside.
- dang 10y ago> 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 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 https://news.ycombinator.com/item?id=11928562 and marked it off-topic.
- tinco 10y agoHi Dang, my apologies, I can no longer edit the comment, please feel free to snip that paragraph out. 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?
- deleted 10y ago[deleted]
- kartickv 10y agoFWIW I didn't interpret this as a personal attack, but as a critical contribution to this discussion: We can't have financial software built by 22-year old dropouts. A new social network? Sure. A game? Sure. A todo list app? Sure. Financial software? No. If it was phrased as "person XYZ is an asshole!" then I would agree that it's a personal attack.
- egg_head 10y agoHe is stating facts, except for the last clause which is an opinion which does not apply to the main subject.
- pmoriarty 10y ago"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." 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.
- vessenes 10y agoWell, Dr. Chris Reitwiessner is in charge of the solidity project I believe. I have been told he's not big on functional / richly typed systems, but I don't have any actual knowledge.
- deleted 10y ago[deleted]