I think he emphasizes the joining of verification and optimization too much. No doubt verification may get easier, if they use the IR and all analysis info the compiler already did. SSA makes this stuff easier for example.
Just tell me what optimization could learn from verification? Everything verification does is too slow to do within a compiler. Sure, you can produce better code, if you are allowed to use NP algorithms, but in reality i have never seen any algorithm more complex than O(n^2) in a compiler. Usually O(nlogn) is the most one can afford.
A deeper understanding of the program - which is what verification brings to the table - may be useful; even if it is too slow for most code, it can occasionally be used to detect bugs/speed up the most critical parts.
It would also be rather useful, although probably quite a bit of work, to have a "verify the optimizations you did" mode. While most errors aren't compiler errors, gcc has been known to optimize bugs into programs...
Just tell me what optimization could learn from verification? Everything verification does is too slow to do within a compiler. Sure, you can produce better code, if you are allowed to use NP algorithms, but in reality i have never seen any algorithm more complex than O(n^2) in a compiler. Usually O(nlogn) is the most one can afford.