Tree Borrows

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.

What you actually want is the underlying separation logic, so you can precisely specify function preconditions and prove mid-function conditions, and the the optomizer can take all those "lemmas" and go hog-wiled, right up to but not past what is allowed by the explicitly stated invariants.

"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".

Can you help me understand your comment with a simple example? Take slice::split_at and slice::split_at_mut:

    fn split_at(&self, mid: usize) -> (&[T], &[T])
    fn split_at_mut(&mut self, mid: usize) -> (&mut [T], &mut [T])

What might their triples look like in separation logic?