Statically sized types in Whiley


#1

The Whiley language (that has extended static verification) has recently introduced RFCs like Rust. Whiley and Rust are two sufficiently different languages, so their needs are sometimes different, but this RFC about statically sized types could be interesting:

Its flow typing allows implicit coercion:

function abs(int:32 x) -> (uint:32 r)
ensures r >= 0:
   //
   if x >= 0:
      return x
   else:
      return -x

In Rust probably you don’t want to add implicit conversions, but you can take advantage of this idea, allowing code similar to:

fn abs(x: i32) -> u32 {
    if x >= 0 {
        u32::from(x)
    } else {
        u32::from(-x)
    }
}

That is a panic-free statically-correct conversion based on some flow typing (then a problem becomes training Rust programmers to avoid the “as” dangerous casts as much as possible).

There is also a paper: http://homepages.ecs.vuw.ac.nz/~djp/files/SEUS15.pdf

Similar flow typing (of slice bounds) is very useful for a more statically-correct handling of slices:

fn foo(a: &[u32; 3]) ->  &[u32; 2] {
    &a[1 ..].as_array()
}
fn main() {
    let b = [10, 20, 30, 40];
    let c = foo(&b[.. 3].as_array());
}

In my code I use slices often, and I’d like to remove some run-time tests and increase static safety of my code.

A better handling of slice bounds also allows to remove some more bound tests during slice/array indexing.