add Stacked Borrows ToC to latest post and expand Stacked Borrows 1 post to hopefully...

[web.git] / ralf / _posts / 2018-11-16-stacked-borrows-implementation.md

diff --git a/ralf/_posts/2018-11-16-stacked-borrows-implementation.md b/ralf/_posts/2018-11-16-stacked-borrows-implementation.md
index 35bf7356f3779c8b2189b6684bd15df98cd21ce5..dbea705eefbe4d9e9518723e9433e9b58901a63d 100644 (file)
--- a/ralf/_posts/2018-11-16-stacked-borrows-implementation.md
+++ b/ralf/_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
 ---
 
 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!
 
 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.
+

 <!-- MORE -->
 
 What Stacked Borrows does is that it defines a semantics for Rust programs such
 <!-- MORE -->
 
 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
 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
 
 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