It seems kind of basic, but I still find myself manually checking code instead of relying on a tool.
It seems kind of basic, but I still find myself manually checking code instead of relying on a tool.
It is possible to determine interesting properties of programs if you weaken your requirements to approximations and/or add significant constraints. You can maintain properties by construction if you only allow yourself to use certain kinds of building blocks in assembling programs. The less powerful your computational model, the easier it is to prove things about it.
The core idea of a type system is to form a symbolic representation of the semantics of your program which is simpler than the program itself, so that you can prove properties of that simpler system instead of the intractable problem of doing so for the actual program. (If you aren't careful, your type system could end up sufficiently powerful that it is itself undecidable, and you're back where you started.)
That theorem proves that no general algorithm exists. That doesn’t mean it can’t be done for a particular program. The real challenge is that modern compilers and processors will execute in a way that is hard to predict from source code.
People don’t do it not only because it’s hard, also because running the function and measuring time + memory is much easier, also much more precise.
Even if you don’t care about time and memory complexity and only care about these useless O(N), it’s still very hard because complexity depends on input data. E.g. bubble sort is O(N^2) but it can also be O(N) if the data is mostly sorted already and only a single element needs to be moved.
https://en.wikipedia.org/wiki/Worst-case_execution_time#Auto...
f(n) = f(n-1) + f(n-1) has runtime O(2^n); f(n) = f(n-1) + f(n-2) has runtmie O(~1.62^n); f(n) = f(n/2) + f(n/2) has O(n log n); for i = 1 to f(n) has runtime f(n).. good luck determining a function output through static analysis
Getting static guarantees about performance would require carefully constructing your code with the tool in mind.
[0] Although I still find it outrageous that CS departments describe their algorithms class as "math" when they do not accept this answer.