Yes, a theoretical calculation like that would be useful as an estimate. But theoretical performance on ideal machines is only loosely related to performance on real machines under real conditions. That's true of testing, too. Benchmark performance varies even between runs.
So there's still going to be a theoretical math versus science and engineering divide.
Another perspective is that we have a useful division of concerns. Static checking is useful to find some kinds of errors. API's help to ensure that certain things don't change in a new version, so that performance improvements are less likely to break callers.
Depending on the domain, leaving some things like performance and size limits deliberately unspecified in API's seems like more of a feature than a bug? Stricter interfaces aren't always an improvement.
> leaving some things like performance and size limits deliberately unspecified in API's seems like more of a feature than a bug
In rare cases there might be exceptions. Hard real time applications and constant time cryptography come to mind.
Regardless, I didn't mean for such proofs to be part of an API or any kind of interface. It's just a guarantee you would get about your program. E.g., "it never times out", or "the worst case data throughout is X" (in whatever hardware model the proof assumes, which in theory could be made very close to the actual hardware).
So there's still going to be a theoretical math versus science and engineering divide.
Another perspective is that we have a useful division of concerns. Static checking is useful to find some kinds of errors. API's help to ensure that certain things don't change in a new version, so that performance improvements are less likely to break callers.
Depending on the domain, leaving some things like performance and size limits deliberately unspecified in API's seems like more of a feature than a bug? Stricter interfaces aren't always an improvement.