I agree with your comment, and I think we are mentioning the same question here, that is essential for the kind of discussion that this article raises - whether

I agree with your comment, and I think we are mentioning the same question here, that is essential for the kind of discussion that this article raises - whether or not a suggested amount of effort to bring Rust into existing and well-established C codebase is a great idea and is justified on a technical merit basis, compared to the effort of brining more sophisticated formal proof assistants that aim at non-intrusive interfacing with C while being productive for the cause of promoting safe and formally-verified programming. Python's gradual typing with MyPy demonstrated a great utility of static type checking that could be brought to existing project through many small and non-desruptive iterations. From my observation an learning of ATS, I expect even greater utility of gradual formal proofs that ATS enables for C. There are tons of successful C codebases, they are used in production around the world and contain a great amount of battle-tested knowledge. They just miss formal proofs that now could be gradually written for them.