alt Hacker NewsIt explains the underlying runtime model they assume, and derives abstractions for the runtime t based on that, which are provably correct up to O(t) under the assumptions.
That does not help you much if you want to know how many seconds this will run. Instead, it tells you the asymptotic runtime complexity of the various algorithms, which is all you can really expect for general functional programs without a concrete machine model.
What I mean is that there is no relationship in Isabelle between their cost function and their actual algorithm.
The process the book goes through for a function f is the following:
1. Define `f`
2. Create a correctness predicate (call it `Correct`) and prove `forall x, Correct(f(x))`
3. Use a script to do some code generation to generate a function `time_f`
4. Prove that `time_f` fulfills some asymptotic bound (e.g. `exists c, forall x, x > c -> time_f(x) < a * x^2`)
Nowhere is `time_f` actually ever formally related to `f`. From Isabelle's point of view they are two completely separate functions that have no relationship to one another. There is only an informal, English argument given that `time_f` corresponds to `f`.
Ideally you'd be able to define some other predicate `AsymptoticallyModelsRuntime` such that `AsymptoticallyModelsRuntime(f, time_f)` holds, with the obvious semantic meaning of that predicate also holding true. But the book doesn't do that. And I don't know how they could. Hence my original question of whether there's any system that lets you write `AsymptoticallyModelsRuntime`.