[nickpsecurity]

There's tools that can prove the absence of runtime errors in industrially-useful subsets of C. Frama-C, RV-Match, and Meta's Infer come to mind. That code is then usable in about anything because so much of it is written in or can call C. Until Rust has that combo, there's still a reason to use C.

Personally, I'd use both Rust and C with equivalent code. The Rust types and borrow checker give some extra assurance that C might not have. The C tooling gives extra assurance Rust doesn't have. Win, win. If I want, I can also do a certified compile or cross-compile of the Rust-equivalent, C code.

[ryao]

Astree claims to be able to prove the absence of runtime errors in both C and C++, without requiring the use of subsets:

https://www.absint.com/astree/index.htm

By the way, C has a formally verified C compiler:

https://compcert.org/compcert-C.html

[nickpsecurity]

Yeah, CompCert will certify a binary for those willing to buy it or use a GPL license. Empirical testing showed it had no bugs in its middle end, unlike other compiler.

On Astree, I couldn't believe it supported all language constructs. I found this on your link:

"and is subject to the same restrictions as Astrée for C.

The high-level abstraction features and template library of C++ facilitate the design of very complex and dynamic software. Extensive use of these features may violate the established principles of safety-critical embedded software development and lead to unsatis­fac­tory analysis times and results. The Astrée manual gives recommendations on the use of C++ features to ensure that the code can be well analyzed. For less constrained (less critical) C++ code, we recommend using the standalone RuleChecker."

So, it still does require a language subset that reduces complexity to benefit from the full analysis. They have greatly expanded what errors they catch since I first read about them. So, thanks for the link.

[koakuma-chan]

I researched and discovered kani https://github.com/model-checking/kani, it's pretty cool.

```rust

#[kani::proof]

fn main() {

    let mut array: [i32; 10] = kani::any();

    array.sort_unstable();

    let index: usize = kani::any_where(|i| *i > 0 && *i < array.len());

    assert!(array[index] >= array[index - 1]);

} ```