[ducktective]

I think it's a given that idiomatic Rust code has less memory bugs than run-of-the-mill C code but IMO, this debate boils down to this question:

"Do static analyzers like cppcheck, Frama-C, Coverity or NASA's ikos catch more bugs (including memory bugs) than idiomatic Rust code?"

We have to consider the added complexity of the Rust language and the massive man-hours required to re-write old C code-bases. It's a trade-off.

[galangalalgol]

From experience, no. At least cppcheck, clang tidy, and coverity together still miss aome fairly simple use-after-free on the stack. Asan or valgrind can catch it, as long as you have a unit test that would cause it, which might require 100% code and branch coverage. In more complicated cases where it somehow dependsnon inputs, even that might not cut it.

[KsassPeuk]

Speaking about tools like Frama-C, it is important to note that while there is an overhead during development of Rust programs because of the type system, proving the absence of runtime errors in industrial size programs using Frama-C is not something easy, and it remains quite costly (and to be fair, far more costly than making Rust programs type). However, it is true that you can catch some errors that are not caught by the Rust type system, say for example, integer overflows. But I would not bet that all problems caugth thanks to the type system of Rust can be caught using Frama-C.

Now, if we focus on functional properties (proving that the code is correct), one terribly hard problem when dealing with real world programs is handling the shape of the memory. That can make some proofs awful and really hard to complete. In a language like Rust, you can get a lot of information about the shape of the memory and the memory separation for free thanks to the type system. That would make proofs really easier (this is for example what is done, but with far less precision than what the Rust type system could provide, in the different memory models configuration in Frama-C/WP and it can already dramatically improve proof performance).

It probably does not justify rewrite everything, nor changing verification tools chains that are in use in some critical domains. However, I would definitely love working on and working with a Frama-Rust tool ;)

[burntsushi]

Yes there are many trade offs to consider and context matters. But that is not the conversation that pclmulqdq is having.