I wonder if Rust or future PL would evolve into allowing multiple borrow checker implementations with varying characteristics (compile speed, runtime speed, algorithm flexibility, etc.) that projects can choose from.
replies(9):
"Rust", in this context, is "merely" "the usual invariants that people want" and "a suite of optimizations that assume those usual invariants, but not more or less".
fn split_at(&self, mid: usize) -> (&[T], &[T])
fn split_at_mut(&mut self, mid: usize) -> (&mut [T], &mut [T])
These functions do not memory accesses, they are both from an operational perspective essentially:
p, n -> (p, p + n)
The separation logics I've seen have all have what we might call a strong extensional calculi / shallow DSL embedding flavor. What that means is roughly that there is strong distinction between the "internal" program under scrutiny, and fairly arbitrary external reasoning about it.
I bring this up in order to say that we're very far from "what is the principal type of this expression?" type questions. There are many, many, ways one might type split_at/_mut depending on what the context requires. The interesting thing about these in Rust is really not the functions themselves, but & and &mut. Those types are stand-ins for some family of those myriad potential contexts, in the way that interfaces are always reifications of the possibilities of what the component on the other side of the interface might be.
In the "menagerie of separation logics" I was originally thinking of, there may not be singular & and &mut that work for all purposes. The most reusable form split_at indeed may be tantamount to the simple arithmetic pure function I wrote above, leaving to the caller the proof of showing whatever properties it needs are carried over from the original pointer to the new ones. Given the arithmetic relations, and the knowledge that nothing else is happening (related to the famous frame rule), the caller should be able to do this.