4 ms·
Rust makes it easy to write code that's very expressive (dynamic memory allocation etc) and has strong safety properties. Certainly easier than having to verify
by roca 6y ago
Rust makes it easy to write code that's very expressive (dynamic memory allocation etc) and has strong safety properties. Certainly easier than having to verify with SPARK or Frama-C. Rust's type system, especially traits and affine types, lets you encode a lot of important properties (e.g. typestates).
Rust does need tools to verify Rust code correctness and especially to verify unsafe Rust code. There is a lot of work going on in this area: see https://alastairreid.github.io/rust-verification-tools/ https://alastairreid.github.io/rust-verification-tools/ for a sample.
- doonesbury 6y agoI'm gonna look at rust; we're a huge c/c++ shop so there's room from improvement here. Now no program is a spec and implementation in one. Thus rust ought to be careful about keeping all it's hammers in language alone. If rust is smart and particularly wants to move to distributed computing or csps correctness will have to take on more complex meanings that bad index or divide by zero.