The Theses
Xr0 is motivated by the following theses:
-
C is the world’s most important language. 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.
-
It is easy to write safe C code in theory, but impossible in practice. The semantics of the C programming language are fairly easy to master, so that for experienced C programmers, the majority of safety bugs occur because of human error rather than genuine misunderstanding. The real challenge in writing safe C is not grasping the rules of, say, the memory model, but manually accounting for uniform, safe application of these rules. The analogy to accounting is highly relevant, in which most of the mathematics is simple arithmetic, but the real difficulties lie in keeping track of large numbers of (individually simple) entities.
-
All that C programmers need, therefore, in order to write well-defined (no UB) programs in C is an accounting tool to help them formalise and verify the interfaces between functions. In keeping with (2.), the only reason mostly safe C programs can be written is programmers are able (albeit with Herculean effort) to structure programs in ways that make the trivial safety bugs obvious. But they are currently powerless against the really subtle safety bugs that arise due to subtle misunderstandings across layers of function calls. This makes it really hard, as Cantrill points out, to compose C programs safely. If we address this loophole by propagating the safety concerns across the interfaces between functions, it will be easy to write safe C.
Intrigued? Read about Xr0’s vision and roadmap to get a sense of how we’re acting in light of these statements.