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.
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
After all, we want miri to also detect UB related to e.g. illegal pointer arithmetic.
These issues are far from settled, and I do have some interesting ideas here that I want so share with you.
-Finally, there is of course the discussion around how to handle raw pointers; I already talked in [§3](#22-unsafe-code) about some of the options that could be explored here.
+Finally, there is of course the discussion around how to handle raw pointers; I already talked in [§2.2](#22-unsafe-code) about some of the options that could be explored here.
Unfortunately, today is the last day of my internship, so I will no longer be able to work on all of this full-time like I did the last three months.
Still, I certainly intend to stay involved. This problem is way too interesting to just let it go :)
-As always, please comment with your thoughts on the topic.
+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**
projects / web.git / blobdiff