(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
## 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:
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
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.
}
{% 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