Xr0 Makes C Safer than Rust
There is a practical way to guarantee the safety of C programs at compile time, in the sense of no use-after-frees, no double frees, no buffer out-of-bounds reads/writes, no null pointer dereferences, no uses of uninitialised memory, no arithmetic overflows/underflows and, more generally, no undefined behaviour. The latest version of Xr0 is an empirical demonstration of the validity of this method. Though very rough around the edges, Xr0 can already eliminate use-after-frees, double-frees, null pointer dereferences, the use of uninitialised memory and memory leaks for a limited subset of C89.
The method is that of formalising and verifying the interfaces between functions. We shall argue that interface informality is the root of all unsafety. The remarkable safety guarantees that Rust provides are consequent to something much deeper than its ownership rules: Rust empowers programmers to formalise and verify the semantics of pointer usage at the interface boundary between functions. If interface formality is the fundamental determinant of safety, systems language design should focus directly on it rather than on any other criterion, including ownership. Xr0 shows how this can be done.
It is simple but expressive, practical but admitting of elegance (think of some of the pointer arithmetic in K&R); it is small, fast, and portable; it is the lingua franca of programming and the language of languages: C is the programmer’s working model for the computer. Good C programmers are, by definition, good programmers. The dominance of the C programming language is no accident and will continue for at least another fifty years.
%20(1).png)
