Live data from Hacker News

Learn Ethereum smart contract programming

ethereumdev.io

191–200 of 244 posts

Re: Learn Ethereum smart contract programming

#191
post #186
post #109

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.....

That's pretty like early days of web development when people write SQL-injection vulnerable code on daily-basis

Re: Learn Ethereum smart contract programming

#192
post #169
post #167

Earlier 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…

Some pointers you might appreciate:

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

#193
post #158

Earlier 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?

because you're shilling for a pyramid scheme , and it's not even a secure pyramid scheme. the software its's built on is shit, from top to bottom.

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

#194
post #109

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…

This would be compelling were it to contain accurate information. However, likening the parity incident to a "hack of ethereum" is like saying the USD is flawed because wells fargo was broken into. The same thing is true for the DAO, although it is indeed more complex in that the _resolution_ of it was handled by Ethereum proper. I think that was questionable.

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

#195

Earlier 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?

>I've been holding a handful of Ethereum since there was a decent dip in the price.

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

#196
post #185

Earlier 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...

That's just an added warning, not a bug fix.

Re: Learn Ethereum smart contract programming

#197
post #136

Earlier 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…

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 halts, period.

Re: Learn Ethereum smart contract programming

#198

Earlier 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.

What proof systems are you thinking about? Strong static types seem the most natural way to introduce formal verification into mainstream programming to me.

Re: Learn Ethereum smart contract programming

#199
post #119

Earlier 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.

Madness indeed. For better or for worse, silly experiments in this industry often turn out to win. According to the "Worse is Better" theory, that's partly because they ship much faster than the projects that want to get everything right, and they're also easier for most people to understand. You could put a team of Ph.D's on inventing a really amazing smart contract formalism based on higher-order zygomorphic type theory, but if only five people in the universe understood it, we wouldn't be talking about it.

Re: Learn Ethereum smart contract programming

#200
post #197

Earlier 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…

> 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 halts, period.

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.

Post reply on HN