Has anyone thought about the possibility of a programming language, and a compiler, such that the compiler can automatically do worst-case asymptotic analysis? The use case I have in mind is a programming language where I write code, and compile. The compiler tells me that my code runs in O(n^2) (for example). It does this by doing what the smart people who do algorithmic analysis do, possibly counting loops and so on.
Because of halting problem issues, and since one can have programs that work by dovetailing, for example Levin's algorithm for SAT that runs in polynomial time iff P=NP, I suspect that one may have to design the programming language to be sufficiently restrictive to allow something like this. Are there negative results, which rule out certain kinds of programming languages from having such compilers.
I would also be interested in systems that give not an exact asymptotic analysis, but an "interesting" upper bound.
I am specifically NOT interested in black box and statistical methods that sample from inputs of particular length, and find out how long the program takes. These methods are very interesting, but they are not what I'm looking for. I am interested in exact methods that may give approximate bounds.
I would be very grateful if someone could point me to some references on work in this direction.