[iainmerrick]

“Formal verification” for Rust code -- does that actually exist yet, or do people just hope/assume that the language will be proven consistent and that awesome theorem-checking tools will emerge eventually?

I agree that Rust has a great model that seems to lead to very solid code, but “formal verification” is a high bar to clear.

[steveklabnik]

We have a dedicated WG now actively working on it https://internals.rust-lang.org/t/announcing-the-formal-veri...

[mikeurbach]

Some people are actively working on formal verification for Rust. The RustBelt project is the first that jumps to mind. A paper and some discussion here: https://news.ycombinator.com/item?id=16302530

[wilun]

Well, you are right, it is not really "formal verification".

But I don't know how to call it, and it is way more checked on some aspects (well, obviously, we are not talking about checking each program against a spec...) that the competition. And by that, I mean that the competition is actually not even trying...