> so the lowest effort path will necessarily involve refactoring it until it does. And that means that rewriting it altogether into a new language has very few

> so the lowest effort path will necessarily involve refactoring it until it does. And that means that rewriting it altogether into a new language has very few drawbacks, and some additional benefits. No, because while some refactoring is necessary, it is virtually always local. E.g. if the sound checker can't prove that an access is within an arrays bounds, adding a dynamic test just before it (assuming you don't want to add annotations to help the checker) will make it provable. Rewriting in a new language is certainly one way to reduce or eliminate memory errors, but if your goal is to reduce or eliminate memory errors in existing codebases, there are other ways that are cheaper, more proven, less risky and are applicable to more environments. These tools are already much more heavily used in safety- and security-critical codebases than any new language, so people are slowly getting good experience with them.