> This makes me wonder: are there any formal specifications on the complexity of this "optimizer as theorem prover"? Basically, the promise here "We formally p

> This makes me wonder: are there any formal specifications on the complexity of this "optimizer as theorem prover"? Basically, the promise here "We formally promise not to promise anything other than the fact that optimized code should have 'broadly' the same effects and outputs as non-optimized code, and if you want to dig into exactly what 'broadly' means prepare to spend a lot of time on it". Not only are there no promises about complexity, there's no promises that it will work the same on the same code in later versions, nor that any given optimization will continue firing the same way as you add code. You can program this way. Another semi-common example is taking something like Javascript code and carefully twiddling with it such that a particular JIT will optimize it in a particular way, or if you're some combination of insane and lucky, multiple JITs (including multiple versions) will do some critical optimization. But it's the sort of programming I try very, very hard to avoid. It is a path of pain to depend on programming like this and there better be some darned good reason to start down that path which will, yes, forever dominate that code's destiny.