3 ms·

Turing completeness isn't so bad when you have a relatively low gas limit on a transaction that ensures you can halt at some point. Maybe I spent too much time

Turing completeness isn't so bad when you have a relatively low gas limit on a transaction that ensures you can halt at some point. Maybe I spent too much time in functional languages and I've been doing too much React stuff lately but the way I see it, we have Contract_method(state, parameters) => {new state, return value} You could always run the program on a fake, mock state then test postconditions for sanity. So, if those postconditions pass and we haven't run out of gas, run the program for real, otherwise return an error. Eg transferring 30 eth from contractA to contractB you would have one of the postconditions asserting that ContractA balance is the old balance minus 30. The notion of gas implies a stack or effort limit, so it's guaranteed that any operation will eventually fail once it runs out of resources. Thus you can specify a theoretical upper limit on resources used in pre-verification, which (AFAIK)is paid by the client contract that requests to withdraw money from the other contract. I guess one could avoid this by using a DSL that is formally verifiable, but it's still an interesting option

dkarapetyan 10y ago
Yes, I'd assumed since Ethereum was so highly touted and hyped that the foundations of the entire thing were sane. Well I mean sane in the sense that the actual contract language was as restrictive as possible and custom made for expressing contract law but it turns out you can do arbitrary computation and although in theory you're limited by this gas thing because the language is not formally specified and verified it is not clear at all if there are no other bugs lurking around with respect to bypassing the gas bounds. What you described is basically abstract interpretation and if it was designed properly then the type system would have taken care of the simulation piece.
- naasking 10y ago
  > What you described is basically abstract interpretation and if it was designed properly then the type system would have taken care of the simulation piece. Actually, termination checkers often compare the size of the term being reduced before and after an evaluation step, and if it can prove that it's always smaller, then termination is assured. With the notion of finite amounts of gas, termination seems assured, so this termination analysis can (and should) be added to EVM. Based on this termination property, all sorts of static analyses now become possible.

dkarapetyan 10y ago

Yes, I'd assumed since Ethereum was so highly touted and hyped that the foundations of the entire thing were sane. Well I mean sane in the sense that the actual contract language was as restrictive as possible and custom made for expressing contract law but it turns out you can do arbitrary computation and although in theory you're limited by this gas thing because the language is not formally specified and verified it is not clear at all if there are no other bugs lurking around with respect to bypassing the gas bounds. What you described is basically abstract interpretation and if it was designed properly then the type system would have taken care of the simulation piece.

naasking 10y ago
> What you described is basically abstract interpretation and if it was designed properly then the type system would have taken care of the simulation piece. Actually, termination checkers often compare the size of the term being reduced before and after an evaluation step, and if it can prove that it's always smaller, then termination is assured. With the notion of finite amounts of gas, termination seems assured, so this termination analysis can (and should) be added to EVM. Based on this termination property, all sorts of static analyses now become possible.