X-Git-Url: https://git.ralfj.de/web.git/blobdiff_plain/b0ae948bd5717d2e779cbae6b9bc1f0498e7ecc5..d08c4b74b314a1f671335ce7986432a58fd1569f:/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 e3ccfd1..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