Re:Bugs that the Rust compiler catches for you
by KsassPeuk on Wednesday May 11, 2022 @10:04AM
(#31340092)
> 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.
Re:Bugs that the Rust compiler catches for you
by kragen on Friday May 13, 2022 @08:52PM
(#31374091)
And vice versa; Frama-C doesn't attempt to prove the absence of data races, last I checked.
Re:Bugs that the Rust compiler catches for you
by KsassPeuk on Monday May 16, 2022 @03:20AM
(#31394360)
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)
However, I also don't think they particularly help you to distinguish a compiler bug from an error in your understanding of the language semantics, although they sure do help a lot with everyday errors.
With respect to questions of inferiority or superiority, keep in mind that Valgrind and UBSan are only dynamic checkers; they don't help at all with errors that don't occur in your testing. Frama-C is a static checker more similar to Rust's capabilities, but much more limited, but also with cscope-like abilities for reverse-engineering existing source bases.
The great advantage these three tools (and ASan) have is that you don't have to rewrite your C in Rust in order to use them.