> Could we define a language so that it uses static analysis to maintain guarantees about a function's use of gas? Have a look at areas like "cost semantics",

> Could we define a language so that it uses static analysis to maintain guarantees about a function's use of gas? Have a look at areas like "cost semantics", e.g. http://lambda-the-ultimate.org/node/5021 http://lambda-the-ultimate.org/node/5021 This takes a language's semantics, i.e. how to evaluate each sort of expression, and extends it to include extra information which can represent time taken, memory usage, cache usage, etc. A simplistic way to track big-O complexity in types is given at http://twanvl.nl/blog/agda/sorting http://twanvl.nl/blog/agda/sorting Note that "gas" systems don't need to produce their result within the given gas limit; it's acceptable for the gas to run out and no value to be produced. This is trivial to prove correct, as it only requires that the language/DSL correctly keeps track of the gas, which can be done "once and for all" since it doesn't have anything to do with whatever algorithm you're writing to use the gas. The machinery for doing that is old hat to functional programming: tracking gas usage is basically a Writer; stopping when gas runs out is basically a Maybe. Statically ensuring that a function is within a gas limit is like statically ensuring that a "Maybe t" value contains a "t" value (as opposed to "Nothing").