& 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).

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.

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.

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.

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.

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.

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. âŠī¸

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!