For a completely arbitrary program, it is not possible to calculate a tight bound on the time or memory complexity of that that program via static analysis. See Rice's Theorem[0].
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.)
> For a completely arbitrary program, it is not possible to calculate a tight bound on the time or memory complexity of that that program via static analysis. See Rice's Theorem[0].
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.
The question was whether it is hard to determine the space/time complexity of ‘a’ function, which firmly placed the question in Rice’s theorem grounds.
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.)
[0] https://en.wikipedia.org/wiki/Rice's_theorem