Rust 2019 -- Correctness and stabilizations

[leonardo]

Last year for Rust 2018 I didn’t write a post like this, hoping to see other people write it. But even with a hundred plus posts that didn’t happen, so this year it’s the moment to speak up.

I have used many different languages in past and when I started studying Rust at version 1.0 I was quickly impressed by its very good design, I was mostly in agreement with most of its design decisions, despite every useful language has a messy implementation. Even small things were designed with care. And I loved how much Rust cares for code correctness. I prefer to avoid long debug sessions and to use more time in the design and coding phases. So I’ve kept learning and using it ever since.

For 2019 and beyond I’d like Rust to keep working on finishing its many unfinished parts. There are lot of unstable features that should be stabilized or modified (or perhaps even closed for now). Keeping features unstable for several years risks making them more like Haskell Language Extensions. Haskell was born to be a testbed for language research, so having lots of implementation-defined Language Extensions could be acceptable for it, but for a more practical language as Rust having features like “slice_patterns” unstable for years is a problem, in my opinion. I now have a ton of code that uses slice_patterns on Nightly, but I don’t know if and how it will keep working.

Beside those stabilizations of unfinished work, I think it’s important for Rust 2019+ to work on improving on one of its main core values, that is correctness. This means that I’d like Rust to improve how reliable it is for basic computing, that means its usage of integral numbers, arrays, slices, vectors (and perhaps even functions). Those are the foundations for most Rust code. Improving reliability for such things is not easy, and it could go against certain usages of Rust. If you are writing quick and small script-like programs then lot of care for correctness could hinder you. So the features that help code correctness should be optional. Only a small subset of code should be at a medium or high integrity level, but Rust should offer well designed optional features for this use case too.

If you take a look at languages designed for maximum reliability, like Ada-SPARK, Spec#, Why3, ATS2 and so on, you see features like contracts to prove correct (as discussed by RustBelt too). But in practice code correctness comes from many other smaller features too, that should be available. So if Rust wants to develop its correctness and to be useful for high reliability usages too it should also improve on its handling of basic constructs like integral numbers, arrays, slices and vectors. There are many small features to do this.

Despite only a small percentage of Rust code needs to be proven correct, the features of Rust to allow this should be usable by a larger group of people. Rust in my vision could help spread the idea of static verification of code, and in general slowly change how programmers and their bosses think about writing system code, to help them care more about formal code correctness.

[crlf0710]

arrays, slices and vectors

and don’t forget tuples. Writing generic code over arrays will be handled by const generics but generic code over tuples are still a mess.

[leonardo]

Is someone able to add a link of this post of mine to this to page?

https://readrust.net/rust-2019/

[bjorn3]

wezm/read-rust/blob/master/.github/contributing.md

[leonardo]

My post was quite vague. This is an example of a hole in Rust handling of arrays that will need to be fixed:

https://www.joshmcguigan.com/blog/array-initialization-rust/

// In some code I've had to create an array with a 3-tuple:

let mut data1: Vec<_> = (b'0' ..= b'9').map(|i| (char::from(i), 0, 0)).collect();

// The successive lines help the type inference specify the type of the second and third tuple integral.
// This code is clear enough, but rustc doesn't perform escape analysis and here it allocates a vec from the heap for something that's better stack-allocated.

// The array is short so a simple alternative version that stack-allocates is to just write down the literal manually:

let mut data2 = [('0', 0, 0), ('1', 0, 0), ('2', 0, 0), ('3', 0, 0), ('4', 0, 0),
                 ('5', 0, 0), ('6', 0, 0), ('7', 0, 0), ('8', 0, 0), ('9', 0, 0)];

// If you don't want to write all the items manually you can use something like this:

let mut data3 = [('\0', 0, 0); 10];
(0 ..= 9).for_each(|i| data3[usize::from(i)].0 = char::from(i + b'0'));

// The third version is OK, but it has some small problems, like having some more bug-prone parts, even if thankfully we manage to avoid casts.

// But in several cases I'd like to create arrays in-place (expecially when they are immutable, unlike here).
// A natural solution is to add syntax that accepts a lambda, but this can't be used because today this already compiles and creates an array with lambdas inside:

let mut data4 = array![|i: u8| (char::from(i), 0, 0), 10];

// So we could add a macro to stdlib, with a bit of compiler support to avoid any copying:

let mut data5 = array![|i: u8| (char::from(i), 0, 0), 10];

[leonardo]

While run-time contract programming is sometimes nice to have, the ability to prove at compile-time the correctness of contracts and specifications is in my opinion a game changer, despite you may want to use it only for important library code (standard library, foundational crates) or critical user functions (important infrastructure software, the kind of code Rust was meant for).

Having ways to prove some indexes can’t go past array bounds or can’t overflow, or some unwraps can’t fail is going to also improve the performance (as long as rustc uses the proof results to optimize better) and not just correctness.

For the correctness part the rustc plugin (like Clippy) discussed here is promising, “Leveraging rust types for modular specification and verification” by Vytautas Astrauskas et al:

https://www.research-collection.ethz.ch/handle/20.500.11850/311092

The syntax shown in that paper currently is:

#[ensures="p.x == old(p.x) + s"]
#[ensures="p.y == old(p.y)"]
fn shift_x(p: &mut Point, s: i32) {
    p.x = p.x + s
}

A more complex example:

#[requires="0 <= n && n < length(r)"]
#[ensures="length(r) == old(length(r))"]
#[ensures="get_nth_x(r, n) == old(get_nth_x(r, n)) + s"]
#[ensures="forall i: i32 ::
    (0<=i && i<length(r) && i != n) ==>
    get_nth_x(r, i) == old(get_nth_x(r, i))"]
fn shift_nth_x(r: &mut Route, n: i32, s: i32) {
    let p = borrow_nth(r, n);
    shift_x(p,s);
}

To improve the readability, improve code aesthetics, and allow syntax highlighting of the contracts and proofs, I’d like a syntax like (like in Why3 language):

fn shift_x(p: &mut Point, s: i32) {
    ensures { p.x == old(p.x) + s }
    ensures { p.y == old(p.y) }
    p.x = p.x + s
}

To allow that we can add some new syntax to Rust:

requires {}
ensures {}
old()
forall i: T :: p1 ==> p2

And little more for explicit proofs, integral intervals, etc.

They have added such syntax to Ada 2012 for similar purposes. Given the correctness purposes of Rust I think this added complexity is worth having (but not right away, putting the contracts and proofs in #[] is OK at the beginning. Ada did the same thing, the contracts were written inside comments before Ada2012).