The "finite time" requirement isn't actually related to performance, it's needed to make sure we can prove meaningful things about the return value. If a functi

The "finite time" requirement isn't actually related to performance, it's needed to make sure we can prove meaningful things about the return value. If a function never returns a value (or it "returns after an infinite amount of time") then anything we say about its return value will be a counterfactual, and open to all kinds of paradoxes and inconsistencies. If we want to enforce some actual performance metric, we can use something like cost semantics ( http://lambda-the-ultimate.org/node/5021 http://lambda-the-ultimate.org/node/5021 ) to enforce complexity bounds (eg. the "big-O" behaviour), then use a few small-scale tests to relate the constant factors in the model to real world values.