I feel that there still is a qualitative difference between & and &Cell: Given a description of the invariants of T, it is in general not possible to derive the invariants of &T. For example, T and Cell<T> (in their “fully owned” variant) have exactly the same invariants; this is also witnessed by the fact that there are functions to convert between the two, and the functions are no-ops. On the other hand, &T and &Cell<T> are clearly very different types.
However, given a description of T, it is actually straight-forward to say what the invariants of Cell<T> and &Cell<T> are.
Of course, interior mutability does extend the power of the language qualitatively, so in some sense Cell is no less fundamental that &. However, this also goes for Mutex and really any other unsafely implemented type that couldn’t also be implemented entirely in safe code. It is perfectly conceivable that there are some specific T that could provide extra operations on Mutex<T>.
Fully agreed.
Cell has to be aware though, as this means the other types rely on the internal invariants of Cell, and not just its public interface.
Wow, I didn’t realize this. Nice! This relies on us knowing the implementation of Rc::clone, and the fact that it could not possibly use another alias of the &Cell, right?
Hm, I wonder how hard it would be to prove these sound in our model…^^