This blog post is very interesting, using Rust’s compiler optimizer as a theorem prover. This makes me wonder: are there any formal specifications on the complexity of this "optimizer as theorem prover"?
Specifically, how does it handle recursion? Consider, for example, the following function, which decrements a number until it reaches zero. At each step, it asserts that the number is nonzero before recursing:
fn recursive_countdown(n: u32) -> u32 {
assert!(n > 0, "n should always be positive");
if n == 1 {
return 1;
}
recursive_countdown(n - 1)
}
Can the compiler prove that the assertion always holds and possibly optimize it away? Or does the presence of recursion introduce limitations in its ability to reason about the program?
> 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.
Compilers can typically reason fairly well about tail recursion like this. In this case the compiler cannot remove the assertion because you could pass in 0. But if you change the assert to be a >= 0 (which is vacuously true, as the warning indicates) it will optimize the code to "return 1" and eliminate the recursive call: https://godbolt.org/z/jad3Eh9Pf
Specifically, how does it handle recursion? Consider, for example, the following function, which decrements a number until it reaches zero. At each step, it asserts that the number is nonzero before recursing:
fn recursive_countdown(n: u32) -> u32 { assert!(n > 0, "n should always be positive"); if n == 1 { return 1; } recursive_countdown(n - 1) }
Can the compiler prove that the assertion always holds and possibly optimize it away? Or does the presence of recursion introduce limitations in its ability to reason about the program?