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])
What might their triples look like in separation logic?