Compiling C to Safe Rust, Formalized

Also, is much of the authors did manual or was it run through something to produce the Rust code? If so, where is the code that generates Rust, I do not see any links to any source repos.

The paper states that these developments will be released under open source licenses after the review process is completed, i.e. most likely, after the paper is formally published.

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"

In this case it's not about Frama-C or similar tools though, see your sibling comments about the caveats.