> I don't understand what this claim is supposed to mean, as there is no standard definition of what "Safe C" consists in. You can prove that some C programs me

> I don't understand what this claim is supposed to mean, as there is no standard definition of what "Safe C" consists in. You can prove that some C programs meet some definitions of safety, and there are memory safe subsets of C. What exactly are you saying isn't possible? What isn't possible is encapsulating many of the safe APIs that Rust supports using C's type system. You can restrict all of the C code in a program to a subset that is safe, but it isn't a subset that anyone actually uses; by contrast, it is absolutely feasible to write programs that use safe Rust outside a handful of unsafe functions in the standard library. The primary reason is that Rust's type system is capable of encapsulating many more safe guarantees than C's is. As someone who works on the RustBelt team, you are misunderstanding the paper. What the paper is arguing is that we need to be able to prove modularity for arbitrary unsafe code, not just treat the standard library as type system primitives, because we want Rust's set of "primitives" to be easily extensible. > The claim that this is fundamentally a kind of verification that you can't do for C or C++ isn't made in the paper. It's not clear to me exactly where this claim is coming from or what precisely it consists in. It is fundamentally different. C++ does not have lifetimes or compile time verification of ownership; its references cannot be safely encapsulated behind an API, and it does not have "modes" like share and own. These are all critical for Rust's safety proofs. This is not for lack of trying; many people have attempted to define safe subsets of C or C++, or add these features to C, such as Cyclone. In all cases, new concepts and types needed to be added to the language and most existing code was no longer usable.