# Why does this refuse to compile?

``````pub struct Vec_Push_Only<'a, T> {
inner: &'a mut Vec<T>,}

impl<'a, T> Vec_Push_Only<'a, T> {
pub fn push(&self, v: T) {
self.inner.push(v)}}
``````

Here is why I expect this to compile: I am NOT changing the value of self.inner (which is a mutable reference to something else).

Why do I need `fn push` to be `&mut self` ?

`&` references are shared references; you can make copies of them (regardless of what they point to). If you could mutate using an `&mut` from inside of `&`, that would break the uniqueness of `&mut`.

In order to mutate, you always need exclusive access (which can be ownership, `&mut`, or something non-primitive like a lock guard).

5 Likes
1. I accept the "proof" as logically watertight.

2. Is this the "most axiomatic" proof?

3. The reason I ask #2 is that this proof is a bit like a "proof by contradiction", i.e.: suppose S was true, then we do this, and now we have a contradiction; therefore S must be false.

Is there a "more direct" way to reason this ?

Mutability is transitive.

In order to mutate something through nested references, every reference along the way needs to be `&mut`. As formulated, your `push()` only gives us a `& &mut T` (via `&self`) and therefore it's not allowed to call any methods on the underlying `T` that require `&mut self`.

1 Like

Here is how I think about the situation;

Taking a &mut reference temporarily takes ownership of the referenced object.

So your struct owns the Vec, just as much as if it wasn't a reference at all.

In order to mutate the objects owned by a struct, you need mutable access to the struct.

So push has to take &mut self.

[ You can get around this using interior mutability, RefCell etc ]

Apologies for being pedantic, is this an 'axiom' of rust borrow checker, or is this some 'higher lemma' that needs it's own proof.

This is deviating a bit from the original question, and even the followup question -- my goal here is not to be obnoxious, but to to build a mental model for quickly evaluating / simulating the borrow checker; I'm trying to figure out a minimal set of "rules" I can memorize, which lets me simulate the borrow checker on small code fragments efficiently.

I'm not quite sure what you are after, but I would probably defer to the Rust Reference here.

Mutability

For a place expression to be assigned to, mutably borrowed, implicitly mutably borrowed, or bound to a pattern containing `ref mut`, it must be mutable. We call these mutable place expressions. In contrast, other place expressions are called immutable place expressions.

The following expressions can be mutable place expression contexts:

• Mutable variables which are not currently borrowed.
• Mutable `static` items.
• Temporary values.
• Fields: this evaluates the subexpression in a mutable place expression context.
• Dereferences of a `*mut T` pointer.
• Dereference of a variable, or field of a variable, with type `&mut T`. Note: This is an exception to the requirement of the next rule.
• Dereferences of a type that implements `DerefMut`: this then requires that the value being dereferenced is evaluated in a mutable place expression context.
• Array indexing of a type that implements `IndexMut`: this then evaluates the value being indexed, but not the index, in mutable place expression context.

(emphasis, mine)

So,

• given "place expressions" (kinda like C++ lvalues) can only be mutably borrowed when it is mutable, and
• The `self.inner` needs to be implicitly mutably borrowed when we call `self.inner.push()` because `push()` takes `&mut self`, and
• In order for a field place expression to be mutable, the subexpression (`self.inner`) must be evaluated in a mutable place context (i.e. `Vec_Push_Only` is borrowed as a `&mut self`)
• This implies `&self` isn't sufficient to call `self.inner.push()`

That's not really a formal proof like you are looking for[1], but that kinda explains the reasoning for my "mutability is transitive" comment.

1. Also, if you are looking for a formal proof you're probably going to be disappointed. Programming languages are a bunch of abitrary rules made up by a distributed group of humans spread across time with loads of edge cases and "implementation defined" behaviour... Properties like "logically consistent/ambiguous/rigorous" are almost always the first things to get sacrificed in favour of ergonomics, backwards compatibility, or performance. âŠī¸

2 Likes

Actually, this is better then what I asked for, it's essentially an algorithm for constructing all "valid &mut"'s. We start with the empty set, then we take the transitive closure of these rules, and the output is the ONLY valid &mut's. Thanks!

2 Likes

This topic was automatically closed 90 days after the last reply. We invite you to open a new topic if you have further questions or comments.