[flagged]
[deleted]
Compiling C to Safe Rust, Formalized
91–100 of 173 posts
Re: Compiling C to Safe Rust, Formalized
#92Earlier 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.
I don't really see it as a big "owning" of Rust that a complex pointer heavy structure with runtime defined ownership cannot be checked statically. Almost every language that people use doubly linked lists in has a GC, making the discussion kind of meaningless.
So C and C++ are the exceptions to the rule, but how do they make it easy to write doubly linked lists? Obviously, the key assumption is that that the developer makes sure that node->next->prev = node->prev->next = node (Ignoring nullptr).
With this restriction, you can safely write a doubly linked list even without reference counting.
However, this isn't true on the pointer level. The prev pointers could be pointing at the elements in a completely random order. For example tail->prev = head, head->prev = second_last and so on. So that going backwards from the tail is actually going forwards again!
Then there is also the problem of having a pointer from the outside of the linked list pointing directly at a node. You would need a weak pointer, because another pointer could have requested deletion from the linked list, while you're still holding a reference.
If you wanted to support this generic datastructure, rather than the doubly linked list you have in your head, then you would need reference counting in C/C++ as well!
What this tells you, is that Rust isn't restrictive enough to enforce these memory safe contracts. Anyone with access to the individual nodes could break the contract and make the code unsafe.
Re: Compiling C to Safe Rust, Formalized
#93The thing I wonder about is why we would do this. The technology to really convert industrial-grade apps from C to Rust could probably bullet proof the C apps more easily. They’d just have to do some analyses that fed into existing tooling, like static analyzers and test generators. Similarly, it they might generate safe wrappers that let teams write new code in Rust side by side with the field-proven C. New code has…
> 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 ex…
> 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.
Re: Compiling C to Safe Rust, Formalized
#94Earlier quoted context omitted.
> I'm not sure what it has to do with translating the code to Rust. Formally verified C programs typically have had all their undefined behaviour already stamped out during the verification process. That makes mapping it over to Rust a lot simpler.
Translating undefined behavior is the easy part.
Maybe, but only if you know the specifics of the environment in which it is executing (i.e. which compiler/architecture-specific behaviours the code actually relies on)
Re: Compiling C to Safe Rust, Formalized
#95I 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…
As I understand it most kernel maintainers aren’t looking to replace C with anything.
Zig has much better interoperability with C than Rust, but it’s not memory safe or stable. I think we’ll see quite a lot of Zig adoption in the C world, but I don’t think it’s in direct competition with Rust as such. In my region of the world nobody is adopting Rust, the C++ people are remaining in C++. There was some interest in Rust originally but it never really caught on in any company I know of. Likely for the same reason Go has become huge in younger companies but will not really make its way into companies which are traditionally Java/C# because even if it made sense technically (and it probably doesn’t) it’s a huge change management task. Zig is seeing traction for programs without the need for dynamic memory allocation, but not much beyond that.
Re: Compiling C to Safe Rust, Formalized
#96The thing I wonder about is why we would do this. The technology to really convert industrial-grade apps from C to Rust could probably bullet proof the C apps more easily. They’d just have to do some analyses that fed into existing tooling, like static analyzers and test generators. Similarly, it they might generate safe wrappers that let teams write new code in Rust side by side with the field-proven C. New code has…
> 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 ex…
> 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...
Re: Compiling C to Safe Rust, Formalized
#97Ugh. 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. Fl…
[deleted]
Re: Compiling C to Safe Rust, Formalized
#98Re: Compiling C to Safe Rust, Formalized
#99Note 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 benefit of compiling formally correct code to Rust? It seems that all the possible benefits are already there (if not more)
Re: Compiling C to Safe Rust, Formalized
#100If you used a naïve translation to Rust, wouldn’t you get parts that are safe and parts that are unsafe? So your manual job would need to be only verifying safety in the unsafe regions (same as when writing rust to begin with)? Seems it would be a win even if the unsafe portion is quite large. Obviously not of it’s 90% of the end result.
A naïve translation would produce rust code which is almost entirely unsafe (using raw pointers instead of references everywhere). Translating to references is difficult, since C code isn't written with the restrictions of the Rust alias model / borrow-checker in mind.