My hope is that giving the programmer more control over optimization, and keeping better track of program properties, would together allow more optimizations that are correct by construction. Like, give the developer visibility into whether an operation is going to be hoisted out of a loop by requiring them to express the fact that it doesn't change (or at least showing them why this was/wasn't inferred). And then a change that makes that stop working could (in the cases where the programmer expressed that they cared about the performance) become a compilation failure rather than a silent performance regression. As a thoroughly trivial example, scala's @tailrec works like this. At the moment it's only really possible because TRO is applied in Scala as a near-syntactic-level transformation rather than a low-level optimization, but if the transformation from syntax to machine code was more gradual and visible, maybe the same kind of thing could be applied more generally, and we could e.g. incorporate performance characteristics into the type system under understandable composition rules.