> but much more limited I agree and I disagree ;) I agree because having a type system that directly provides the guarantee that whole classes of runtime erro

> but much more limited I agree and I disagree ;) I agree because having a type system that directly provides the guarantee that whole classes of runtime error cannot happen provides fast feedback during development at a low cost. I disagree because even in a press button (+ tuning) approach, you can prove things with Frama-C that the Rust compiler cannot prove (reason why there is runtime bound-checking, implementation defined behavior for integer overflow and so on in Rust). But also because you can prove much more advance properties than "just" absence of runtime errors.