alt Hacker News> If the abstraction maintains the properties you care about, PROVABLY, there is no problem.
This approach doesn't do that. The translation from the actual executing code to the representation used for runtime analysis is done entirely informally and not checked at all by Isabelle.
It 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.