I wrote a new daemon in C the other day. Plenty of people will continue to write software in C. Some will even write it in C++. There is nothing you can write that will convince the world to stop writing software in these languages. We went through this once with Java. We are going through it with Rust. We will go through it with Zig or whatever it is that people say everyone should adopt next instead of Rust and all else that came before it.

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.

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

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.

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]);

} ```

I do, and will, the industry does and will, for at least a few more decades. And I even enjoy doing so (with C; C++ is more forced upon me, but that'll be the case for some time to come)

That’s what I’m saying. By a few decades you and most of those alleged 7 million C/C++ developers will retire and there won’t be anyone to replace them because everyone will be using Rust or Zig or Go.

Very strong statement, one I don't really believe

That’s what happened to COBOL, right?

In COBOL’s case, nobody really wanted to write software in it in the first place. People used assembly or FORTRAN at the time. MBAs wanted a language corporate secretaries could use, so they made COBOL. It failed at its main purpose, but since IBM pushed it for business processing, people were coerced into writing software with it since if they did not use it, they would not have a job. As the industry developed, they stopped finding new people that they could coerce into using it and the old people started retiring/dying. Unlike COBOL adoption, C and C++ adoption occurred because software engineers wanted to use them due to merit.