Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Compiling C to Safe Rust, Formalized

arxiv.org

Post reply on HN
Print view View original

81–90 of 173 posts

Re: Compiling C to Safe Rust, Formalized

#81

Post by 3836293648 »

zoom6628 wrote: post #55

I wonder how this compares to the zig-to-C translate function. Zig seems to be awesome at creating mixed environs of zig for new code and C for old, and translating or interop, plus being a C compiler. There must be some very good reasons why Linux kernel maintainers aren't looking to zig as a C replacement rather than Rust. I don't know enough to even speculate so would appreciate those with more knowledge and exper…

Zig isn't 1.0 and has zero backcompat guarantees. It's also barely used anywhere and hasn't proven its value, even if parts of it may seem promising

Re: Compiling C to Safe Rust, Formalized

#82

Post by zozbot234 »

PhilipRoman wrote: post #79
jokoon wrote: post #74

Earlier quoted context omitted.

What is formally verified C? Why isn't there more of it?

Because it takes a lot of effort. Google Frama-C. On the flip side, it can express not just memory safety constraints, but also correctness proofs. In this case it's not about Frama-C or similar tools though, see your sibling comments about the caveats.

Arguably, generating verified C from a low-level focused subset of F* (Low*, used in the HACL project) is close enough to count as a "similar tool".

Re: Compiling C to Safe Rust, Formalized

#84

Post by lou1306 »

light_hue_1 wrote: post #77
wffurr wrote: post #6

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.

Oh, this has so so many more caveats! It's borderline false advertising. 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…

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

Re: Compiling C to Safe Rust, Formalized

#85

Post by light_hue_1 »

lou1306 wrote: post #84
light_hue_1 wrote: post #77

Earlier quoted context omitted.

Oh, this has so so many more caveats! It's borderline false advertising. 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…

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

> Er, this I can understand. Every conference paper only presents you with a simplified view of the contributions.

In my group I don't allow hacks. Most other good papers I can think of don't do that. It takes new students a while to get used to not maximizing performance at all costs. And if a hack must exist, then it's explained, not as a hack, but as part of the method.

Don't you hate it when you implement some beautiful idea from a paper only to discover that it hardly bares any relationship to the actual method that works?

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

You're probably right. But POPL allows for unlimited pages in an attached appendix. They can and should describe the full method. Particularly if they're going to play the game of saying that they formalized this.

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

It's a form of namespace squatting. Do the worst job possible to claim a title that you couldn't execute on, so that when people figure out that problem, they will be forced to cite your non-working solution. I loathe this approach to publishing.

We should punish people for doing. Reject for lack of honesty and your paper can't be published in related conference for X years.

Re: Compiling C to Safe Rust, Formalized

#87

Post by kelnos »

Ugh. They didn't compile any C to Rust. They modified the F*-to-C compiler to emit Rust instead. So they compiled F* to safe Rust. And they couldn't even do that 100% reliably; some valid F* constructs couldn't be translated into Rust properly. They could either translate it into Rust code that wouldn't compile, or translate it into similar-looking Rust code that would compile, but would produce incorrect results.

Flagged, this is just a lie of a title.

Re: Compiling C to Safe Rust, Formalized

#88

Post by shakna »

josefx wrote: post #70
ChristianJacobs wrote: post #60

Earlier quoted context omitted.

> looking to zig as a C replacement rather than Rust Rust isn't a "replacement for C", but an addition to it. It's a tool that Torvalds et. al. has recognised the value of and thus it's been allowed in the kernel. The majority of the kernel code will still be written in C. I'm no kernel maintainer, but I can speculate that two of the main reasons for Rust over Zig are the compile time guarantees that the language pro…

> It's a tool that Torvalds et. al. has recognised the value of and thus it's been allowed in the kernel. Has there actually been a successfull contribution to the mainline kernel? The last two big projects I heard of (ext2 / Apple drivers) seemed to have issues getting their code accepted.

rnull is in the kernel. And I believe one of the generic Realtek drivers is Rust as well.

Re: Compiling C to Safe Rust, Formalized

#89

Post by PartiallyTyped »

akkad33 wrote: post #83
wffurr wrote: post #6

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.

Is Rust formally verified? Not that I know of

You can always run model checkers like Kani, though even that is limited.

Re: Compiling C to Safe Rust, Formalized

#90

Post by bonzini »

saghm wrote: post #51
oneshtein wrote: post #43

Earlier quoted context omitted.

It's easy to implement doubly linked lists in safe Rust. Just ensure that every element has one OWNER, to avoid «use after free» bugs, or use a garbage collector, like a reference counter. Unlike C++ or Rust, C has no references, only pointers, so developer must release memory manually at some arbitrary point. This is the problem and source of bugs.

While I might agree that it's easy if you use a reference counter, this is not going to be as performant as the typical linked list written in C, which is why the standard library uses unsafe for its implementation of stuff like this. If it were "easy" to just write correct `unsafe`, then it would be easy to do it in C as well. Note that the converse to this isn't necessarily true! People I trust way more to write un…

> unsafe Rust can be harder than writing C in some ways due to having to uphold certain invariants that don't come up in C.

Yes, this is absolutely correct and on top of this you sometimes have to employ tricks to make the compiler infer the right lifetime or type for the abstraction you're providing. On the other hand, again thanks to the abstraction power of Rust compared to C, you can test the resulting code way more easily using for example Miri.

Post reply on HN