[KsassPeuk]

> 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.

[kragen]

And vice versa; Frama-C doesn't attempt to prove the absence of data races, last I checked.

[KsassPeuk]

In fact there exists a plugin that can do that but it is currently not free:

https://frama-c.com/fc-plugins/mthread.html

(And by the way since it is not done by typing it is hard to use on legacy code)