Can one automate algorithmic analysis? 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.
Implicit Complexity has taught us that (some) complexity classes can be classified by type systems, in the sense that there are type systems that only accept polynomial programs, for example. One more practical-minded offshoot of this research is RAML (Resource Aware ML), a functional programming language with a type system that will give you precise information of the running times of its programs. It is more precise, in fact, than big-O complexity, are constant factors are also included, parametrized by a cost model for the base operations.

You may think that this is cheating: surely some algorithms have a complexity that is very hard to compute precisely, so how could this language easily determine the complexity of its programs? The trick is that there are many ways to express a given algorithm, some which the type-system will reject (it rejects some fine programs), and some, maybe, that it accept. So the user doesn't get the world for free: he or she doesn't have to compute cost estimations anymore, but need to figure how to express code in a way that is accepted by the system.

(It is always the same trick, as with programming languages with only terminating computations, or provable security properties, etc.)