X-Git-Url: https://git.ralfj.de/web.git/blobdiff_plain/74654295059da58bf9376a2d06bcbb231f1adcfb..3b92763e32c9d13a80fe4ab85037d5ea4eb20c69:/personal/_posts/2017-08-11-types-as-contracts-evaluation.md diff --git a/personal/_posts/2017-08-11-types-as-contracts-evaluation.md b/personal/_posts/2017-08-11-types-as-contracts-evaluation.md index edb2a45..68318a6 100644 --- a/personal/_posts/2017-08-11-types-as-contracts-evaluation.md +++ b/personal/_posts/2017-08-11-types-as-contracts-evaluation.md @@ -4,7 +4,7 @@ categories: internship rust forum: https://internals.rust-lang.org/t/https-www-ralfj-de-blog-2017-08-11-types-as-contracts-evaluation-html/5753 --- -Some weeks ago, I described [Types as Contracts]({{ site.baseurl }}{% post_url 2017-07-17-types-as-contracts %}) as an approach for how to go about defining Rust's aliasing-related [undefined behavior]({{ site.baseurl }}{% post_url 2017-07-14-undefined-behavior %}). +Some weeks ago, I described [Types as Contracts]({% post_url 2017-07-17-types-as-contracts %}) as an approach for how to go about defining Rust's aliasing-related [undefined behavior]({% post_url 2017-07-14-undefined-behavior %}). One key property of this approach is that it is *executable*, which means we can actually have a program (in this case, [miri](https://github.com/solson/miri/)) tell us whether some particular Rust test case exhibits undefined behavior or not. I have since then spent most of my time completing and refining this implementation, and running it on miri's test suite to exercise various bits of the standard library and see whether they are actually following the rules I have been suggesting. @@ -19,7 +19,7 @@ Finally, I discuss some of the things that I would like to look at going forward Unsurprisingly, some of miri's test cases started to fail once I properly implemented the rules I wanted to have checked. Some of these turned out to be [compiler](https://github.com/rust-lang/rust/issues/43457) [bugs](https://github.com/rust-lang/rust/issues/43481), but others are actually examples of code violating the proposed rules. In the following, I describe the patterns that I found. -I assume that you are familiar with Types as Contracts as introduced in my [previous post]({{ site.baseurl }}{% post_url 2017-07-17-types-as-contracts %}). +I assume that you are familiar with Types as Contracts as introduced in my [previous post]({% post_url 2017-07-17-types-as-contracts %}). ### 1.1 Ownership Passing Via Raw Pointers @@ -268,4 +268,4 @@ Still, I certainly intend to stay involved. This problem is way too interesting As always, please [comment](https://internals.rust-lang.org/t/https-www-ralfj-de-blog-2017-08-11-types-as-contracts-evaluation-html/5753) with your thoughts on the topic. I am particularly curious about what kind of test cases you are throwing at miri, and how it is doing! -**Update**: I added a proposal for how to fix the `Arc` problem. +**Update:** I added a proposal for how to fix the `Arc` problem. **/Update**