Compiler Verification

The tools can help you move back and forth between these two. I think it's beautiful mathematically,. but there are so many ways in which it helps in practice, and that's why i find it really fun to work ont. To step back fora moment, it sounds like some of your frustration with working on this verification style approach is not serving the actual needs of developers. In part because as correctness wasn't quite as high on their list of requirements for them to put the amount of effort required to use these formal techniques. This leads me to ask about something that you've worked on, which is super optimization - an example of a compiler technique where correctness becomes incredibly critical. So maybe