X-Git-Url: https://git.ralfj.de/web.git/blobdiff_plain/187a862323d9120c30bd4824ad6f8760e84c91a4..effa50ab9673f8313069ee8cbbe85665cdb329fc:/personal/_posts/2018-11-16-stacked-borrows-implementation.md?ds=sidebyside diff --git a/personal/_posts/2018-11-16-stacked-borrows-implementation.md b/personal/_posts/2018-11-16-stacked-borrows-implementation.md index 35bf735..dbea705 100644 --- a/personal/_posts/2018-11-16-stacked-borrows-implementation.md +++ b/personal/_posts/2018-11-16-stacked-borrows-implementation.md @@ -4,16 +4,21 @@ categories: internship rust forum: https://internals.rust-lang.org/t/stacked-borrows-implemented/8847 --- -Three months ago, I proposed [Stacked Borrows]({% post_url -2018-08-07-stacked-borrows %}) as a model for defining what kinds of aliasing -are allowed in Rust, and the idea of a [validity invariant]({% post_url -2018-08-22-two-kinds-of-invariants %}) that has to be maintained by all code at -all times. Since then I have been busy implementing both of these, and +Three months ago, I proposed Stacked Borrows as a model for defining what kinds +of aliasing are allowed in Rust, and the idea of a [validity invariant]({% +post_url 2018-08-22-two-kinds-of-invariants %}) that has to be maintained by all +code at all times. Since then I have been busy implementing both of these, and developed Stacked Borrows further in doing so. This post describes the latest version of Stacked Borrows, and reports my findings from the implementation phase: What worked, what did not, and what remains to be done. There will also be an opportunity for you to help the effort! +This post is a self-contained introduction to Stacked Borrows. Other than +historical curiosity and some comparison with my earlier work on +[Types as Contracts]({% post_url 2017-07-17-types-as-contracts %}) there is no +reason to read the [original post]({% post_url 2018-08-07-stacked-borrows %}) at +this point. + What Stacked Borrows does is that it defines a semantics for Rust programs such @@ -29,9 +34,9 @@ help us. We have to define a set of rules that makes sense even for unsafe code. I will explain these rules again in this post. The explanation is not going to -be the same as last time, not only because it changed a bit, but also because I -think I understand the model better myself now so I can do a better job -explaining it. +be the same as [last time]({% post_url 2018-08-07-stacked-borrows %}), not only +because it changed a bit, but also because I think I understand the model better +myself now so I can do a better job explaining it. Ready? Let's get started. I hope you brought some time, because this is a rather lengthy post. If you are not interested in a detailed description of