4 ms·

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

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.