> 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.
This simply says that functional languages could be assigned cost semantics, just like imperative languages have, and so may be used for algorithm analysis. It has nothing to do with verification.
> tracking gas
Yep, but that's a trivial property that could be done by any runtime. It doesn't help prove any other correctness property.
Have a look at areas like "cost semantics", e.g. 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
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").