[drdeca]

Well, the compiled code is available, and if they provide the source code, you can verify that it compiles to the code on chain (or, you can analyze the code on chain without the source code of the contract, but that is harder).

The source code for the contract can be made to have a proof of correctness in it, or, as it is probably not all that long, if you look at the source code long enough you can be sufficiently convinced that it runs how you expect it to.

Regarding the problems with turing completeness, any transaction is guaranteed to finish within a particular number of steps, because the transaction includes an amount of "gas", which puts a limit to how many steps the contract will run. If it runs out of gas before finishing, all the changes in the state are reverted (but the person still pays the gas cost). If it finishes, then the extra "gas" is returned. (the transaction specifies some "gas cost", which is how much ether per gas or gas per ether (idr) , and some amount of ether, which is the max cost the transaction is allowed to take. There aren't "gas balances", any "gas" that is transferred just is ether at the end. Its just a unit of how much computation, and the gas price is how much they are willing to pay per amount of computation. I feel like I didn't explain this well...)

Checking that the contracts were run correctly is done by anyone verifying the block which contains the contract call. If the miner runs the contract incorrectly, then the people verifying the block will not accept the block as valid, so people won't mine on the block, so it wont end up in the main chain, so the miner will not receive anything from mining the block, and what happens in the wrong execution wont effect anything.

I'm not sure if this explanation has been very clear, but I hope it has been clear enough. I can try again if it isn't though.

[mannykannot]

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.

[drdeca]

Afaik, no, proofs of correctness are not currently implemented in the languages that are used. Some of them iirc have a way to do that in part, but currently the languages aren't set up for full proofs of correctness. (But, iirc, some things can be shown)

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.

[nivertech]

I think @mannykannot misunderstands the purpose of gas in Ethereum. It's only purpose is a solution to the Halting Problem [1]. Alternative solution could be disallowing jumps backwards / loops or limiting time of the computation.

Why is it the problem? Because contract with something like while(1){}; will render the entire network of nodes useless.

1. https://en.m.wikipedia.org/wiki/Halting_problem

[mannykannot]

I am well aware of the purpose of gas. What I have not seen is any argument (from @drdeca or anyone else) that gas materially simplifies the problem of verifying that a contract behaves properly (from your perspective, as one of the parties to the contract) in all circumstances. The fact that it will always halt is only a tiny step along that road, and if it halts as a result of running out of gas, that is strong evidence that it has not worked as intended.

An example may be useful. Suppose I tell you that I have written an Ethereum contract whereby people can loan me money, and after a year, I will pay them back double. Before you enter into one such contract with me, I hope it would cross your mind to wonder if I might actually be running a Ponzi scheme. Don't worry, I say, Ethereum has this gas feature that means the transaction will always halt. How much more confident should that information make you feel?

As for your alternatives, gas is essentially the same as limiting the time of computation. If backwards jumps were disallowed, the language would not be even approximately Turing-equivalent.

[nivertech]

1. Gas mechanism has nothing to do with tamper-proofing transactions, thats what blockchain (or more correctly hashchain) is for.

2. There are Turing-complete languages which only allow loops with known number of iterations.

3. Check my presentation, If you want to understand Ethereum programming model:

http://www.slideshare.net/mobile/nivertech/ethereum-vm-and-d...

IMO Ethereum is just a first step in the right direction, the real solution will need to be much more scalable.

[mannykannot]

> 1. Gas mechanism has nothing to do with tamper-proofing transactions, thats what blockchain (or more correctly hashchain) is for.

I am not sure why you are mentioning this here, but if this is what you think I am misunderstanding about gas, perhaps you could point out where you think I made this mistake.

>2. There are Turing-complete languages which only allow loops with known number of iterations.

You did not originally write "loops with known number of iterations", you wrote "disallowing jumps backwards / loops".

> 3. Check my presentation, If you want to understand Ethereum programming model.

Based on your contributions to this thread so far, I am not very confident that I will find my specific question addressed, but if you give me a specific slide number to start at, I will give it a look.

BTW, do you have an answer to the question I posed in the second paragraph of my previous post?

[Retra]

You can only create a little trust by reading source code. You really have to analyze the whole compilation processes.