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").
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.
And we usually don't wait that long. A function that executes when loading a web page times out in the order of seconds.
Once you have deadlines, all bets are off - the function is not deterministic for any large enough input. Equational reasoning does not preserve performance - it could cause a program that previously ran fast enough to time out.
So, knowing that function terminates seems only theoretically useful. It doesn't tell us whether a program change is really safe. It would be more useful to put some kind of bound on the resources a function can consume.
In Etherium's language, there is a concept of "gas" which is an abstract limit on how much work a function can do. (The advantage over a timeout is that it's not machine-specific.) I sometimes wonder if anyone has applied this concept to functional programming? Could we define a language so that it uses static analysis to maintain guarantees about a function's use of gas?