Awesome! One thing, though - in reading through it, the signature of the WhyML in the “Related Work” section doesn’t seem to match the Rust code you give.
The Rust you give is:
fn get_mut<T>(slice: &mut [T], index: usize) -> &mut T
while the WhyML is
let get_mut (a: array (ref int)) (i: int) : ref int = a[i]
let get_mut (a: array int) (i: int) : ref int = ref a[i]
However (depending on the semantics of WhyML, which I am not familiar with), those seem like they’d be more similar to the following:
fn get_mut(a: Rc<[&mut i32]>, index: usize) -> &mut i32;
fn get_mut(a: Rc<[i32]>, index: usize) -> &mut i32;
and that a more accurate analogy might be
let get_mut (a: ref (array int)) (i: int) : ref int = ref a[i]
(Which would still return a copy, thus preserving your point that WhyML does not permit all of the niceties that Rust’s references do).