The sad reality of Ethereum: 1. Bitcoin is slow and expensive, Ethereum is the future 2. Ethereum software has security hole, gets hacked 3. Ethereum fans say it's an experiment there are lots of things that will transform Ethereum (Casper/PoS, Raiden, zkSNARKs, Enterprise Alliance) 4. Low price getting pumped by Ethereum Foundation & big-holder affiliates 5. Back to #1 We've seen it happen again (DAO) and again (Par…
> Ethereum software has security hole, gets hacked The exploits so far were NOT security holes in ethereum, they were poorly written smart contracts by third parties.....
Learn Ethereum smart contract programming
191–200 of 244 posts
Re: Learn Ethereum smart contract programming
#192Earlier quoted context omitted.
If you're competent with proofs in Idris, you can write your EVM programs as an Idris DSL. But, I mean, there's no proof that the Idris compiler does what it's supposed to do, so you'd still have a huge trusted base.
> If you're competent with proofs in Idris, you can write your EVM programs as an Idris DSL. Yeah, all my formal proof experience is with Coq, which is just a bit too idiosyncratic and difficult for this sort of thing. But I seem to remember that—especially if you're willing to certify specific results , and not necessarily the program in general—you can make your trusted computing base very small indeed. I mean, if…
Jack Petterson and Robert Edström did a master's thesis about retargeting the Idris compiler to emit EVM code, with a custom effect type to express smart contract effects. They ended up modestly skeptical of functional programming as a paradigm for EVM, instead looking toward process calculi. https://publications.lib.chalmers.se/records/fulltext/234939...
Yoichi Hirai's summary of his research into Ethereum formal verification as a full-time formal methods researcher at the Foundation: https://github.com/pirapira/ethereum-formal-verification-ove...
See especially his formalization of the EVM as Hoare triples in Lem, which is usable from Isabelle: https://github.com/pirapira/eth-isabelle -- very cool stuff, although I have to say that the ostensible complexity and difficulty of his proof verifying an utterly simple wallet contract makes me a bit skeptical of this approach to smart contract correctness: https://github.com/pirapira/eth-isabelle/blob/master/example...
Re: Learn Ethereum smart contract programming
#193Earlier quoted context omitted.
>"I've been holding a handful of Ethereum since there was a decent dip in the price. I haven't spent much time on it and I have no good leads for program ideas yet, but if the code is buggy and I get hacked and lose my investment, that's fine. A smart contract is a project, and it could fail like any other. Don't put your retirement savings in a smart contract right now unless you're OK with losing it all. Maybe in t…
Why are you sick of hearing it? Why are you even in this thread? If ethereum is so dumb, why do you care so much?
The people writing programs on it are writing bad programs.. but even if they write them well the environment has vulnerability built into it .
>Why are you even in this thread?
Why are you here? it's one of the top posts on this site today.
Re: Learn Ethereum smart contract programming
#194The sad reality of Ethereum: 1. Bitcoin is slow and expensive, Ethereum is the future 2. Ethereum software has security hole, gets hacked 3. Ethereum fans say it's an experiment there are lots of things that will transform Ethereum (Casper/PoS, Raiden, zkSNARKs, Enterprise Alliance) 4. Low price getting pumped by Ethereum Foundation & big-holder affiliates 5. Back to #1 We've seen it happen again (DAO) and again (Par…
Literally no one within Ethereum calls it an experiment. You have to cherry-pick from population and then ascribe it to the whole for this to be even sensical.
Essentially every technology we can think of can be rooted back to the 90s, or really any period we want to look at since that is how knowledge works. If you've got a particular, say it...rather than just this poor, lazy attempt at a sort of character assassination by employee (fairly inaccurate) appeal to oldness.
It is thoroughly _without merit_ to suggest that the analogous components of ETH and BTC have BTC being more secure. In fact, the opposite is true by any reasonable measure. Further, there are indeed things that Ethereum tries to do that add complexity, but if they come with value we shouldn't then find ourselves saying things like you do that amount to a sort of "my abacus is more secure than quickbooks online" - different purposes, solving different problems and creating different sorts of value. Even beyond that BTC holds all records for security events and $ cost of them, coin-loss amounts of of them, and so on.
Re: Learn Ethereum smart contract programming
#195Earlier quoted context omitted.
>"I've been holding a handful of Ethereum since there was a decent dip in the price. I haven't spent much time on it and I have no good leads for program ideas yet, but if the code is buggy and I get hacked and lose my investment, that's fine. A smart contract is a project, and it could fail like any other. Don't put your retirement savings in a smart contract right now unless you're OK with losing it all. Maybe in t…
Which part do you have a problem with?
You opened by explain how you clearly have an interest in this, you got in, and since you are saying you bought during a "decent dip" that means you only got in recently.
The rest of your post would be shilling only that you disclosed your interest.
Re: Learn Ethereum smart contract programming
#196Earlier quoted context omitted.
Looking at Solidity's release log, the last update was 18 days ago. It fixed some minor bugs from the previous release three days prior, and none of the bugfixes mentioned in the previous release seem to fit your description. Do you have a link? https://github.com/ethereum/solidity/releases
A look at the recent commits would suggest they are correct: https://github.com/ethereum/solidity/commit/e506129aee5745e2...
Re: Learn Ethereum smart contract programming
#197Earlier quoted context omitted.
The real answer is probably that total languages are obscure and the Ethereum inventors didn't know about them so they chose a simple and ordinary stack machine. But those total systems are, of course, subsets of Ethereum, which means that if you write your program in an obviously finite way, you can use the same inductive proofs you would use for a total language. Turing completeness makes it hard to prove propertie…
> The real answer is probably that total languages are obscure and the Ethereum inventors didn't know about them so they chose a simple and ordinary stack machine. I'm not an expert on Ethereum, but even if they did pick a total language, how would you deal with bounding the CPU cost of complex contracts? Even if you could formally verify a loop would eventually terminate, wouldn't long running loops or those with ex…
Re: Learn Ethereum smart contract programming
#198Earlier quoted context omitted.
> The real answer is probably that total languages are obscure and the Ethereum inventors didn't know about them so they chose a simple and ordinary stack machine. I'm not an expert on Ethereum, but even if they did pick a total language, how would you deal with bounding the CPU cost of complex contracts? Even if you could formally verify a loop would eventually terminate, wouldn't long running loops or those with ex…
I'm not sure static typing is tied to formal verification. In fact if you think about it most proofs are basically typeless I a lot of cases.
Re: Learn Ethereum smart contract programming
#199Earlier quoted context omitted.
The belief that Turing machines aren't amenable to formal verification is a hobgoblin that shows up in every thread like this, but it's not real. Of course there are limited formalisms that make certain types of verification easier, but proving programs has been possible since, like, the 1960s. A multisig, for example, has a finite number of states when considered under symbolic execution. A model checker can rip thr…
> Should Ethereum not have been launched until it had solid methods for auditing and proving? Maybe, but that's not how the world works, typically. Worse is better and all that. As a platform for experimentation that's fine. As a platform for doing real things with meaningful amounts of money, it's madness.
Re: Learn Ethereum smart contract programming
#200Earlier quoted context omitted.
> The real answer is probably that total languages are obscure and the Ethereum inventors didn't know about them so they chose a simple and ordinary stack machine. I'm not an expert on Ethereum, but even if they did pick a total language, how would you deal with bounding the CPU cost of complex contracts? Even if you could formally verify a loop would eventually terminate, wouldn't long running loops or those with ex…
The gas limit is one reason I think it's weird that people insist on calling the EVM "Turing complete", since one of the most prominent features of the system is that every program is guaranteed to terminate in a finite and low number of steps (via the gas mechanism). Turing complete programs are supposed to be problematic because of the halting problem, but in the EVM, the halting problem is trivial: every program h…
Exactly, knowing that the contract code will eventually halt is nice to know but knowing that it will halt after a reasonable CPU cost seems much more important in this case (which is really interesting).
From what I've seen from example contracts, it doesn't seem like the chance of infinite loops is that high. Personally, I find that in mainstream languages, if you accidentally write an infinite loop you find out very quickly on the first few runs and code that could be hiding an infinite loop stands out. The vast majority of loops just iterate from the start of a collection to the end.