7 ms·
To 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
by whazor 10y ago
To 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.
- jacquesm 10y ago> Ethereum is a turing machine that runs code 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.
- lomnakkus 10y agoNot sure why you're being downvoted. This is the problem. 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.
- quonn 10y ago> 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. 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.
- egg_head 10y agoWhen I had my own start up companies or worked for those of my friends, we ensured that the first few sets of big customers got white glove treatment from the executive team.... This is what happens when one does not do that. :)