Comment by auggierose

> I don't understand the relevance. I'm not asking for exact computation of steps. Big O is fine. And provisional on the current implementation would be the whole point.

What do you mean by "the current implementation"? Isabelle defines mathematical functions, not running code.

> No. That would be a clear hack. And it would break a lot of stuff in Isabelle.

You are thinking a little bit too simplistic here. Of course you have to do some work to integrate it properly. In particular, you would need to have to generate inequalities (upper bounds) as runtime theorems. Just as code generation (for example to Ocaml) is integrated with Isabelle, this approach could be integrated similarly, and I don't think there would be any danger to the logic. Note that for code generation, you also have to provide special theorems for higher-order functions. But it would definitely be interesting to work this out in detail.

> wouldn't be able to state or prove very natural theorems such as "the asymptotic runtime of a sort function based on pairwise comparison can't be less than O(n log(n))"

No, you wouldn't, because the approach only proves upper bounds. As stated before. So lower bounds on runtime complexity would not be natural at all in this framework.

> The problem isn't axiomatic vs definitional, the problem is denotational vs operational.

You have to explain what you mean by that. Of course you can write these morphisms, you need to define your machines and machine functions first though, which is a lot of work. Maybe start with just a Turing machine first. The upside of all this work: you could also prove theorems about lower bounds now.