You can also say that for JavaScript, and see how successful TypeScript is.

Yes, you can rewrite everything in Elm, PureScript or even anything that is more similar to JS, but step by step conversion to TS enables a significant quality improvement for large codebases (I personally think it doesn't fare so well on small codebases, where there are some people who use it even for one-off scripts, but at least we can agree on large codebases I think)

> You can also say that for JavaScript, and see how successful TypeScript is.

I'm not sure that's what you meant, but interoperability between C and Rust does seem to be a selling point of Rust (like TS and JS), and allows C codebases to be oxidized gradually rather than rewritten from scratch.

But you can't just add types to C and it becomes rust. It needs serious refactoring. You'd probably go lib by lib, whereas you can rename a JS file to TS and it starts checking types (even without, if you configure it that way).

By the way, I love rust, but I just don't understand the "rewrite all the things" hype. Being battle tested means a lot for low-level libs. You can't guarantee that you ported everything exactly, with bugs and all. Pragmatic solutions like "Checked C" prove a lot in that regard.

> you can't just add types to C and it becomes Rust

You actually can “just” turn C into Rust with something like c2rust. But you haven't gained any safety without refactoring.

Is that not also the case for Checked C?

You cannot be sure that you kept 100% of the semantics when you use c2rust. You need to focus on semantics plus the types. With checked c, you can just keep your focus on the types.

TypeScript doesn't have to solve memory safety problems because JavaScript effectively does not have them. Marking whether things are strings, integers or objects is a much easier problem than e.g. assigning correct lifetimes to C pointers.

> 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.

I’m not sure what C code bases you’ve worked with but refactoring in a large C code base is almost never local. Especially if it’s a code base that made extensive use of the gcc flags that disable making sure code does not alias.

Providing enough information for the prover does not require a big refactoring, and is significantly cheaper and less risky than a rewrite for an established codebase.