At some point, in order to make C safer, you're going to have to introduce some way of writing a more formal specification of the stack, heap and the lifetime of references into the language.

Maybe that could be through a type system. Maybe that could be through a more capable run-time system. We've tried these avenues through other languages, through experimental compilers, etc.

Without introducing anything new to the language we have a plethora of tools at our disposal:

- Coq + Iris, or some other proof automation framework with separation logic.

- TLA+, Alloy, or some form of model checking where proofs are too burdensome/unnecessary

- AFL, Valgrind and other testing and static analysis tools

- Compcert: formally verified compilers

- MISRA and other coding guidelines

... and all of this to be used in tandem in order to really say that for the parts specified and tested, we're confident there are no use-after-free memory errors or leaks. That is a lot of effort in order to make that statement. The vast, vast majority of software out there won't even use most of these tools. Most software developers argue that they'll never use formal methods in industry because it's just too hard. Maybe they'll use Valgrind if you're lucky.

Or -- you could add something to the language in order to prevent at least some of the errors by definition.

I'm not a big Rust user. Maybe it's not great and is too difficult to use, I don't know. And I do like C. I just think people need to be aware that writing safe C is really expensive and time consuming, difficult and nothing is guaranteed. It might be worth the effort to learn Rust or use another language and at least get some guarantees; it's probably not as hard as writing safe C.

(Maybe not as safe as using Rust + formal methods, but at least you'll be forced to think about your specification up front before your code goes into production... and where you do have unsafe code, hopefully it will be small and not too hard to verify for correctness)

Update: fixed markup