From: Ralf Jung Date: Sat, 15 Jul 2017 17:43:29 +0000 (-0700) Subject: wording X-Git-Url: https://git.ralfj.de/web.git/commitdiff_plain/80c8c2547685046f77d14c63682e60d723a6cd62 wording --- diff --git a/personal/_drafts/types-as-contracts.md b/personal/_drafts/types-as-contracts.md index 5b1974f..89d99b3 100644 --- a/personal/_drafts/types-as-contracts.md +++ b/personal/_drafts/types-as-contracts.md @@ -60,7 +60,7 @@ The validation of reference types (in particular, their exclusive / read-only na The extra state in my proposal consists of something akin to a reader-writer lock for every memory location. I am first going to describe these locks and how they affect program behavior, before explaining contract validation. -[^1]: If at this point you are under the impression that all these previous posts have been just building up and are now coming together in this proposal, you are not entirely wrong. +[^1]: If at this point you are under the impression that all these previous posts have been collectively building up towards this proposal, you are not entirely wrong. ### Memory locks diff --git a/personal/_posts/2017-07-14-undefined-behavior.md b/personal/_posts/2017-07-14-undefined-behavior.md index ae5463e..e93a608 100644 --- a/personal/_posts/2017-07-14-undefined-behavior.md +++ b/personal/_posts/2017-07-14-undefined-behavior.md @@ -55,7 +55,7 @@ Undefined behavior moves the burden of proving the correctness of this optimizat 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. @@ -87,4 +87,4 @@ Such a specification would describe the additional state that is needed at run-t 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.