Why does this refuse to compile?

1 
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 ?

2

& 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
3

  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 ?

4

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
5

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 ]

6

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.

7

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
8

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
9

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.