> A far more feasible approach (though still very expensive) -- and probably a more "correct" one, even theoretically -- is to verify existing C code using some

> A far more feasible approach (though still very expensive) -- and probably a more "correct" one, even theoretically -- is to verify existing C code using some of the many excellent verification tools (from static analysis to white-box fuzzing and concolic testing) that exist for C[1]. Most static analysis tools for C suck: (0) Few of them are actually sound. An unsound tool is basically worthless if you really want to be sure that your code has no errors. (1) They suffer from modularity issues. As you say, they rely on analysis of the control flow of the program (abstract interpretation), which means that, more often than not, the different parts of your program end up related by monstrous preconditions and invariants that expose more implementation details than any sensible programmer would like. (2) Finally, from a purely pragmatic point of view, they impose the burden of “jumping” between more levels of abstraction: C's syntax (which is already two-layered, thanks to the C preprocessor), some hopefully correct formal semantics for C, and whatever concepts (e.g., sets of states characterized by an invariant) that formal semantics is defined in terms of. With type systems: (0) We have a methodology (due to Wright and Felleisen) for proving that a language is type safe. (1) The type system's intrinsic complexity establishes an upper bound on how intricate the interfaces between modules can be. (2) For the most part, the programming only needs to care about the denotation of syntax in terms very close to the problem domain. The actual boring syntax processing is the type checker's job. > It is more "correct" because, while perhaps not providing some of the other benefits, those tools can prove more properties than the Rust type system can, and such tools don't (yet) exist for Rust. Using a single formal system to prove absolutely everything is impractical. Some things are more convenient to enforce mechanically and internally: (0) Case analysis exhaustiveness: Humans are comically bad at this. OTOH, it's very easy for a type checker to make sure that a pattern matching block has an arm for every constructor of an algebraic data type. (1) Separation of concerns: Parametric type abstraction guarantees that abstraction clients aren't exposed to the implementor's design choices. While other things are easier to prove manually and externally: (0) Equational laws: Not all algebraic theories are decidable, which means that there's no single search procedure that can decide whether a given equation (with all free variables implicitly universally quantified at the beginning) follows from others. (1) Routine invariants that are obvious by inspection, and would be too burdensome to annotate in the syntax of a program.