3 ms·
“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
by iainmerrick 9y ago
“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.
- wilun 9y agoWell, 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...
- mikeurbach 9y agoSome 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 https://news.ycombinator.com/item?id=16302530
- deleted 9y ago[deleted]
- steveklabnik 9y agoWe have a dedicated WG now actively working on it https://internals.rust-lang.org/t/announcing-the-formal-verification-working-group/7240 https://internals.rust-lang.org/t/announcing-the-formal-veri...