Considering that the compiler can only be so smart, this is a great way to justify optimizations that would otherwise be difficult or impossible to perform.
Unfortunately, it is often not easy to say whether a program has undefined behavior or not -- after all, such an analysis being difficult is the entire reason compilers have to rely on UB to perform their optimizations.
Furthermore, while C compilers are happy to exploit the fact that a particular program *has* UB, they do not provide a way to test that executing a program *does not* trigger UB.
-It also turns out that programmers' intuition often [does not match what the compiler does](https://www.cl.cam.ac.uk/~pes20/cerberus/notes50-survey-discussion.html), which leads to miscompilations (in the eye of the programmer) and sometimes to security [vulerabilities](https://lwn.net/Articles/342330/).
+It also turns out that programmers' intuition often [does not match what the compiler does](https://www.cl.cam.ac.uk/~pes20/cerberus/notes50-survey-discussion.html), which leads to miscompilations (in the eye of the programmer) and sometimes to security [vulnerabilities](https://lwn.net/Articles/342330/).
As a consequence, UB has a pretty bad reputation.
There are various sanitizers that watch a program while it is being executed and try to detect UB, but they are not able to catch all possible sources of UB.
It is with such considerations in my mind that I have previously written about [miri as an executable specification]({{ site.baseurl }}{% post_url 2017-06-06-MIR-semantics %}).
Coming up next on this channel: During my [internship]({{ site.baseurl }}{% post_url 2017-05-23-internship-starting %}), I am working on such a specification.
-I have a draft ready now, and I want to share it with the world to see what the world thinks about it.
+I have a draft ready now, and I will share it with the world to see what the world thinks about it.