Popular posts

We hope so! We're currently working with academics to define and verify the language itself; once we do that, we'll see what the future holds :) It's on a long timeframe though.

I definitely think Rust can be very helpful here. The same rules around aliasing and mutation that come from ownership + borrowing can also help a formal verification tool track the current state of a value in a more detailed way. But I don't know of any tools that are usable at this very moment for doing this sort of thing with Rust code (*). It's always been a dream of mine, however, to deploy tools like that on the standard library and other widely used bits of unsafe code.

(*) EDIT: As others noted, there are some in development.

Yes, absolutely! We're actually working with a number of academic and industrial groups in this realm to uncover the potential there.

It's unclear whether this verification work will ever become part of the core language, or always remain an additional tooling layer. But regardless, the Rust type system provides, by construction, a lot of information that you otherwise have to work very hard to get via static analysis.

I'd expect to see some initial forrays here as early as 2018.