Live data from Hacker News

Compiling C to Safe Rust, Formalized

arxiv.org

51–60 of 173 posts

Re: Compiling C to Safe Rust, Formalized

#51

Earlier quoted context omitted.

No one here is confused about what unsafe means. The point is, they're not implemented by following Rust's ownership model, because Rust's ownership model does in fact forbid that kind of thing. You can nitpick the meaning of "forbids", but as far as the current context is concerned, if you translate code that implements a doubly linked list (as opposed to using one from a library) into Rust, it's not going to work w…

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 unsafe Rust code than me than me have argued that 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. While there are a number of blog posts on the topic that anyone interested can probably find fairly easily by googling "unsafe Rust harder than C", I'll break my usual rule of strongly preferring articles to video content to link a talk from youtube because the speaker is one of those people I mention who I'd trust more than me to write unsafe code and I remember seeing him give this talk at the meetup: https://www.youtube.com/watch?v=QAz-maaH0KM

Re: Compiling C to Safe Rust, Formalized

#53
post #27
post #23

Earlier quoted context omitted.

> Rust’s ownership model forbids things like doubly linked lists, which C programs use a lot. It’s literally in the standard library https://doc.rust-lang.org/std/collections/struct.LinkedList....

This implementation uses unsafe. You can write a linked list in safe rust (e.g. using Rc), but it probably wouldn't resemble the one you write in C. In practice, a little unsafe is usually fine. I only bring it up since the article is about translating to safe rust.

More important than whether you use a little unsafe or a lot, is whether you can find a clean boundary above which everything can be safe. Something like a hash function or a block cipher can be piles and piles of assembly under the covers, but since the API is bytes-in-bytes-out, the safety concerns are minimal. On the other hand, memory-mapping a file is just one FFI function call, but the uncontrollable mutability of the whole thing tends to poison everything above it with unsafety.

Re: Compiling C to Safe Rust, Formalized

#54
post #49
post #42

Earlier quoted context omitted.

> The exercise here is to auto-identify-and-refactor idioms open-coded in one language, into idioms suited for the other language's already-written standard library. That's what LLMs are for - idiom translation. You can't trust them to do it right, though. [Pan et al . 2024] find that while GPT-4 generates code that is more idiomatic than C2Rust, only 61% of it is correct (i.e., compiles and produces the expected res…

Oh god, I can't even imagine trying to have formally-verified LLM-generated code. It's not surprising that even incremental progress for that would require quite a lot of ingenuity.

[deleted]

Re: Compiling C to Safe Rust, Formalized

#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 experiencing weighing in.

Re: Compiling C to Safe Rust, Formalized

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

What is the main difference? Can compiler flags force compliance?

"Formally verified" means someone has written a correct mathematical proof that the code has no bugs (the proof is checked by a computer program to make sure it is correct). This is a very high bar.

I'm not sure what it has to do with translating the code to Rust.

Re: Compiling C to Safe Rust, Formalized

#57
post #42

Earlier quoted context omitted.

But it's not in C's standard library. So the exercise isn't merely to auto-translate one language's standard library to another language's standard library (say, replacing C++ std::list with Rust LinkedList) — which would already be very hard. The exercise here is to auto-identify-and-refactor idioms open-coded in one language, into idioms suited for the other language's already-written standard library. Imagine refa…

> The exercise here is to auto-identify-and-refactor idioms open-coded in one language, into idioms suited for the other language's already-written standard library. That's what LLMs are for - idiom translation. You can't trust them to do it right, though. [Pan et al . 2024] find that while GPT-4 generates code that is more idiomatic than C2Rust, only 61% of it is correct (i.e., compiles and produces the expected res…

Actually, LLMs are for generating humorous nonsense. Putting them in charge of the world economy was not intended, but we did it anyway.

Re: Compiling C to Safe Rust, Formalized

#59

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…

Maybe because zig isn't memory safe.

Re: Compiling C to Safe Rust, Formalized

#60

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…

> 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 provides being better as well as the rate of adoption. There is a lot of work done by many leading companies in the industry to provide Rust native code or maintained Rust bindings for their APIs. Windows devs are re-writing parts of _their_ kernel in Rust. There's a "movement" going on that has been going on for a while. I only hope it doesn't stop.

Maybe the maintainers feel like Zig doesn't give them enough over C to be worth the change? Many of them are still opposed to Rust as well.

Post reply on HN