I feel like we need for C and C++ what Typescript is for Javascript: Not a language from scratch but something which is as close as possible to the thing everyone is familiar with while doing the thing Rust does. A standard library where everything has the same names, the same kind of C++ objects and templates and RAII etc., change only this and nothing else.
Because otherwise you make people learn 100 other things at once to start using it effectively, and then they don't.
That isn't the thing Rust does, and is slower, so then people won't use it.
The advantage of Rust is that you can produce efficient safe code. The disadvantage is that you have to learn a different language first, which deters adoption.
Zig is something like this for C, but not C++. There are a number of ongoing attempts to do something like this for C++, but it is very hard and they are all way behind Rust in terms of mindshare.
Check out the tooling from the seL4 project.
I'm aware they used intermediate levels between raw C and the proof assistant, but I don't see why that should be prohibitive.
Because otherwise you make people learn 100 other things at once to start using it effectively, and then they don't.