Something I've mused about is whether it would be possible to reason about performance characteristics at a types level, to statically identify things like quad

Something I've mused about is whether it would be possible to reason about performance characteristics at a types level, to statically identify things like quadratic behavior. No idea what this would look like; I just see this gap where type systems have gotten quite good at ensuring against incorrectness (not C's, of course, but that's another discussion), but there's almost no equivalent story for catastrophic performance regressions, which in some cases can be just as serious as a program-crashing bug. Basically when it comes to performance we're still in the place that we used to be with correctness: "either read the entire stack of source code to understand everything that's happening, or try and remember to read the docs which may or may not be correct and exhaustive and just hope for the best". The performance characteristics of a piece of code are part of its contract with the outside world, but that contract is in no way formalized right now.