| Thank you for your reply, but I have to say that I think it understates the problem. >The source code for the contract can be made to have a proof of correctness in it.. Has this capability already been implemented for the Ethereum contract language(s)? If so, I would greatly appreciate a link, as my admittedly cursory search did not find it (there is some discussion of verification of the Ethereum infrastructure, but that is merely a precondition to contract verification.) Even so, I think it is significant that only a tiny fraction of today's software is written this way, and only a tiny fraction of all developers know how to do it. Someone has to write these contracts. >... or, as it is probably not all that long... Ethereum's promoters are imagining nothing less than a revolutionary new economy, with vast networks of interacting contracts. The amount of contract software implicit in these dreams is huge. >If you look at the source code long enough you can be sufficiently convinced that it runs how you expect it to. The steady stream of security vulnerabilities that are being found in ordinary software shows that this is not an effective technique. If you are a software developer, imagine doing your work in an environment where any bug of yours could cause you, personally, to lose a significant amount of money. Nor do I think 'gas' completely solves this problem. Now your analysis has to cover the issue of whether your contract, or any of those it is dependent on, will run out of gas before completion. In most cases, and particularly in networks of dependent transactions, reverting back to the initial state is not a viable outcome (imagine that happening on the last payment of your mortgage on a house.) I can imagine that running out of gas on some obscure corner case might be used by an attacker as as a means to disrupt a network of dependent transactions. |
It is planned though.
Ok, yes, I suppose that the contracts will/would eventually get kind of long. As it is now though, It hasn't taken me /all/ that long to read the contracts I've looked at. (But perhaps I've only bothered to look at the ones short enough to read )
Regarding finding security flaws despite people looking carefully: yes, that seems a good point. I think proofs of correctness will be important for important contracts. However, many contracts logic is not really all that complicated. A contract can be powerful without being complicated, I think. Because of this, I think much of the time the proofs should not be too hard to write.
Regarding running out of gas:
Well, yes, if the transaction you send does not have enough gas, and you needed it to run, that could be a problem. But, if you run the transaction locally, and use that to estimate the amount of gas which needs to be used (might not be exact if the state of the contract changes in a way that your transaction needs more computation, but for reasonable contracts I think this would not be much), and one can provide extra gas in case this happens (the extra gas will be refunded), to have a high confidence that it will be enough.
But, if the transaction is important, one would be watching what happened carefully anyway, to make sure the transaction gets in the chain, regardless of the complications from the computations in the transaction. If, counter to your expectations, the gas you provided did not end up being enough, then you would be able to notice this, and, though you would be out that gas cost, you could just send the transaction again with more gas.
The block times are very short (under a minute), so you probably wouldn't have to wait long to send the transaction again with more gas. Most of the gas costs shouldn't be too large, so unless the transaction you are sending is very time sensitive, or very computationally expensive, a transaction running out of gas shouldn't be /too/ much of a problem?
I think you make some good points btw, just explaining my understanding of how those things are addressed.
Also, I'm not sure, but it seems you might have a small confusion about gas. Gas is included in the transaction, not stored by a contract over time. Gas only exists within the context of a particular transaction, the token which is actually exchanged is ether. You might have just been choosing not to mention the details of that though.