say immutable instead of read-only
authorRalf Jung <post@ralfj.de>
Thu, 15 Nov 2018 12:50:28 +0000 (13:50 +0100)
committerRalf Jung <post@ralfj.de>
Thu, 15 Nov 2018 12:50:28 +0000 (13:50 +0100)
personal/_drafts/stacked-borrows-implementation.md

index ac3624da458cb6f07dcbdef4773b8d483fd8f327..1bc1ef12d0012fd0a09d20eaf6209b2d547947c8 100644 (file)
@@ -20,7 +20,7 @@ that some things about references always hold true for every valid execution
 (meaning executions where no [undefined behavior]({% post_url
 2017-07-14-undefined-behavior %}) occurred): `&mut` references are unique (we
 can rely on no accesses by other functions happening to the memory they point
 (meaning executions where no [undefined behavior]({% post_url
 2017-07-14-undefined-behavior %}) occurred): `&mut` references are unique (we
 can rely on no accesses by other functions happening to the memory they point
-to), and `&` references are read-only (we can rely on no writes happening to the
+to), and `&` references are immutable (we can rely on no writes happening to the
 memory they point to, unless there is an `UnsafeCell`).  Usually we have the
 borrow checker guarding us against such nefarious violations of reference type
 guarantees, but alas, when we are writing unsafe code, the borrow checker cannot
 memory they point to, unless there is an `UnsafeCell`).  Usually we have the
 borrow checker guarding us against such nefarious violations of reference type
 guarantees, but alas, when we are writing unsafe code, the borrow checker cannot
@@ -39,7 +39,7 @@ you only want to know how to help, jump to [section 6].
 
 ## 1 Enforcing Uniqueness
 
 
 ## 1 Enforcing Uniqueness
 
-Let us first ignore the part about `&` references being read-only and focus on
+Let us first ignore the part about `&` references being immutable and focus on
 uniqueness of mutable references.  Namely, we want to define our model in a way
 that calling the following function will trigger undefined behavior:
 
 uniqueness of mutable references.  Namely, we want to define our model in a way
 that calling the following function will trigger undefined behavior:
 
@@ -163,7 +163,7 @@ If we just had unique pointers, Rust would be a rather dull language.  Luckily
 enough, there are also two ways to have shared access to a location: through
 shared references (safely), and through raw pointers (unsafely).  Moreover,
 shared references *sometimes* (but not when they point to an `UnsafeCell`)
 enough, there are also two ways to have shared access to a location: through
 shared references (safely), and through raw pointers (unsafely).  Moreover,
 shared references *sometimes* (but not when they point to an `UnsafeCell`)
-assert an additional guarantee: Their destination is read-only.
+assert an additional guarantee: Their destination is immutable.
 
 For example, we want the following code to be allowed -- not least because this
 is actually safe code accepted by the borrow checker, so we better make sure
 
 For example, we want the following code to be allowed -- not least because this
 is actually safe code accepted by the borrow checker, so we better make sure
@@ -634,7 +634,7 @@ the stack, such that the access through `mut_ref` at the end remains valid.
 This may sound like a weird rule, and it is.  I would surely not have thought of
 this if `RefCell` would not force our hands here.  However, as we shall see in
 [section 5], it also does not to break any of the important properties of the
 This may sound like a weird rule, and it is.  I would surely not have thought of
 this if `RefCell` would not force our hands here.  However, as we shall see in
 [section 5], it also does not to break any of the important properties of the
-model (mutable references being unique and shared references being read-only
+model (mutable references being unique and shared references being immutable
 except for `UnsafeCell`).  Moreover, when pushing an item to the stack (at the
 end of the retag action), we can be sure that the stack is not yet frozen: if it
 were frozen, the reborrow would be redundant.
 except for `UnsafeCell`).  Moreover, when pushing an item to the stack (at the
 end of the retag action), we can be sure that the stack is not yet frozen: if it
 were frozen, the reborrow would be redundant.
@@ -786,7 +786,7 @@ fn demo_mut_advanced_unique(our: &mut u8) -> u8 {
 }
 {% endhighlight %}
 
 }
 {% endhighlight %}
 
-### 5.2 Shared References (without `UnsafeCell)` are Read-only
+### 5.2 Shared References (without `UnsafeCell)` are Immutable
 
 The key property of shared references is that: After creating (retagging,
 really) a shared reference, if we then run some unknown code (it can even have
 
 The key property of shared references is that: After creating (retagging,
 really) a shared reference, if we then run some unknown code (it can even have