Compiling C to Safe Rust, Formalized

> The technology to really convert industrial-grade apps from C to Rust could probably bullet proof the C apps more easily.

No, some C programs cannot be made safe. This can be due to dependency on undefined or unspecified behaviors, or it can be because introducing proper safety checks would limit the domain of possible inputs too much to be useful, or other things.

Translating to a safe language can maintain the expressive capabilities of the inputs while statically guaranteeing correct operation at run-time. It is objectively better in these cases.

> field-proven C

I don't think this exists, as the numerous critical vulnerabilities over the years have shown. All we have is C that seems to work pretty well often enough to be useful.

> old code is proven safe

Old code is assumed to be safe due to luck, actually. "Prove" has a specific meaning (especially on a post for a paper about proving things), and the overwhelming majority of C code is not proven to any rigorous mathematical standard. In contrast, the Rust type system has been mathematically proven to be correct.

> A full on translator might be an ideal option.

It depends on what you're willing to give up. If you don't mind losing performance, limiting your domain of inputs or range of outputs, giving up code legibility, and so on, then sure, this can probably be done to some extent. But when you start wanting your translator to be both sound and complete over all of these concerns, you run into problems.

> No, some C programs cannot be made safe. This can be due to dependency on undefined or unspecified behaviors, or it can be because introducing proper safety checks would limit the domain of possible inputs too much to be useful, or other things.

You can certainly replace code using undefined behavior in C code by using defined constructs.

> I don't think this exists, as the numerous critical vulnerabilities over the years have shown. All we have is C that seems to work pretty well often enough to be useful.

I think this highly misleading. Some of the most reliable programs I know are written in C and Rust projects will also have critical vulnerabilities. Most vulnerabilities are not actually related to memory safety and the use of unsafe Rust will also lead to memory safety issues in Rust code. So I see some advantage to Rust but to me it is obviously overhyped.

> In contrast, the Rust type system has been mathematically proven to be correct.

Is this the case? E.g. the issue "Prove the Rust type system sound" https://github.com/rust-lang/rust/issues/9883 is closed with comment "This will be an open issue forever. Closing." in 2016: https://github.com/rust-lang/rust/issues/9883#issuecomment-2... .

At least nowadays (since 2022) we do have a language specification for Rust: https://ferrous-systems.com/blog/the-ferrocene-language-spec...

The closest thing is probably RustBelt [0], which proved the soundness of a subset of Rust that included borrowing/lifetimes. This was later extended to include relaxed memory accesses [1].

Neither of these papers include the trait system, unfortunately, and I'm not aware of another line of research that does (yet?).

[0]: https://dl.acm.org/doi/10.1145/3158154

[1]: https://plv.mpi-sws.org/rustbelt/rbrlx/paper.pdf

There’s tools that prove the safety of C code. They include RV-Match, Astree Analzer, and Frama-C. CompCert certifies the compilation. There’s tons of tools to find bugs by model checking, test generation, etc. Rust was nowhere near C last I checked in terms of tooling available.

So, back to my original comment, the investment in making a Rust to C transpiler would make a C to safer C transpiler that fed that code into the verification tooling. A small transpiler would be easier to write with huge, immediate gains.

On field proven, there’s two angles: spec and code. Many C/C++ apps didn’t become usable at all until years of iteration based on feedback from field use. An alternative in Rust might have incorrect specs which. From there, a number have had much code review, static analysis, and testing. They have few to no known bugs at any point. So, there are definitely C/C++ applications out there that are field-proven with a decent level of safety.

(Note: Any transpiler might need to be bug for bug and weird behavior for weird behavior compatible to match the implicit spec in the C/C++ code.)

You’re right about the average Rust vs C code, like type system vs correctness. I’d prefer new code be written in safer languages, which I added to my proposal.

If apples to apples on correctness, you’d have to compare C written for verification with Rust. Quite a few C projects have been proven to be correct. Since you’re using a compiler, I’ll add that tools like Softbound+CETS make C code safe automatically.

I do think Rust brings the cost and effort down quite a lot, though. It’s tooling is usually more mature or at least free than most for verifying C.