Note that this is done for “existing formally verified C codebases” which is a lot different from typical systems C code which is not formally verified.
replies(8):
First of all they never translated any C! At all. Zero lines.
They took code written in F* and modified its C compiler to emit Rust. They never had to deal with any actual C code of any complexity, aside from the most trivial code that might theoretically be emitted by a toy compiler (but wasn't even that!). They just pretended they were dealing with C (or a heavily restricted Mini-C).
Even if we accept this, there are plenty of arbitrary restrictions on the C it can even support in principle:
> If the original C program further relies on x, our translation will error out, and will ask the programmer to fix their source code.
That's saying you want C to already be written in a style that makes the Rust borrow checker happy! They're avoiding the actual hard parts of the problem.
> These rules present simplified versions of what we support. Our implementation features several peephole optimizations ...
If I may translate from the language of academia. "We present beautiful rules in figure 4. But in reality, our implementation relies on a large number of hacks."
But it gets worse!
> For overlap cases that can be distinguished statically (as above), we emit a compile-time error; otherwise, the Rust code will panic at runtime.
The resulting code is not guaranteed to be correct! For example, aliasing in C can cause crashes in the resulting Rust code. See comment at the top of page 10. We're going from a formally verified C program to a "It may crash now" Rust program!? That's nuts!
> We apply our methodology to existing formally verified C codebases, namely, the HACL* cryptographic library ...
This is such a blatant lie that I had to return to it. It's designed to catch an unwary reviewer. We often talk about HACL being in verified C because it gets compiled to that. But it's not a C library, it's written in a totally different language. You cannot confuse the two.
I'm not a reviewer for their paper. But if I was, I would strongly fight for rejection.
The fact that they only handle formally verified C is so astronomically far away from being their main problem.
An honest title would be "Compiling a subset of F* to partially Safe Rust, Partially Formalized"
Sadly that is the name of the game in conference publishing. Make a big claim in the title and hope the reviewer does not read the fine print.
> If I may translate from the language of academia. "We present beautiful rules in figure 4. But in reality, our implementation relies on a large number of hacks."
Er, this I can understand. Every conference paper only presents you with a simplified view of the contributions. There is no way to describe every corner case within the page limits of a conference paper (specifically, I bet this was submitted to POPL 2025).