Live data from Hacker News

Compiling C to Safe Rust, Formalized

arxiv.org

161–170 of 173 posts

Re: Compiling C to Safe Rust, Formalized

#161
Author here, I thought it'd be helpful to address a few of the points brought up in the various comment threads.

1. This is an academic paper that we posted on arxiv, not a release announcement for a new product where we claim we have solved C to Rust. We submitted to a PL conference, not an open-source meeting like e.g. FOSDEM -- this is not the same audience at all, and the expectations are very different.

2. Our story is simple. We start from the constraint of translating C to /safe/ Rust, and see what this entails: a small well-behaved subset of C, inference of slice splitting, a translation that may error out, and a program that may abort (plus a few other things described in the paper). We evaluate our ideas on what we have (C embedded in F*), and show that it scales decently with those constraints in mind, on a large-scale C library that is used in Firefox, Python, and many other pieces of mainstream software. We don't claim we can rewrite e.g. Firefox in Rust automatically.

3. This is how research works. We think we have an interesting point in the design space; we don't claim we solve every issue, but think this is an interesting idea that may unlock further progress in the space of C to Rust translation, and we think it's worth putting out there for others to take inspiration from. Who knows, maybe some existing tool will use this approach for parts the fit in the subset, and fall back to unsafe Rust for other parts that don't fit! This is a very active area: if we can contribute something that other tools / researchers can use, great.

4. This is not the final story, and again this is how research works. We are working on an actual C frontend via libclang, and are exploring how e.g. guarantee that the generated Rust does not generate out of bounds accesses, perhaps by emitting verification conditions to Z3 (speculating on future work here). If the reviewers think more work is needed, that's fine, and we'll resubmit with enhancements. If the reviewers think this is an active area and others could benefit from our ideas, and take the paper, even better.

Re: Compiling C to Safe Rust, Formalized

#162

Earlier quoted context omitted.

So no?

The answer is that it is not. It frustrates me more than it should, I admit, that people always mention Rust when they talk about safety, but never Ada / SPARK. You want formal verification? Use Ada / SPARK. It has been battle-tested. It has been used for critical systems for a really long time now. (And a compiler being formally verified vs. being able to write formally verified code means two different things.)

[deleted]

Re: Compiling C to Safe Rust, Formalized

#163

Earlier quoted context omitted.

Rust is to safe as Tesla is to autopilot.

Judging by the facts, are you saying that Tesla has a safe auto pilot? Rare to see on HN :^)

Heh no... I was going for "the average person thinks Rust is automatically safe." And "the average person thinks Tesla is automatically safe."

Re: Compiling C to Safe Rust, Formalized

#164

[flagged]

With rust having recently entered the Linux kernel, Windows 11, qemu among others where Haskell never took a hold, I really fail to see where you feel the wind is blowing. The thing is, rust is used today in more and more places because it's reliable. We're not going to switch out the ground we are standing on every time something shiny comes along and that's why this is such an interesting development.

Just because you have tiny pieces being written in it doesnt mean its getting adopted. Its way too cumbersome to write entire OS in it - all the example projects like AWS Firecracker end up with tons of unsafes. And its runtime components for dynamic memory stuff eat into efficiency.

Basically a more expansive and possibly ML powered valgrind can easily offer the same memory safety as Rust does, without the penalty of slower development and efficiency hits, so Rust adoption is "unstable" i.e its just a nice improvement but not does not give a hard advantage in any form and way.

Re: Compiling C to Safe Rust, Formalized

#165

[flagged]

What steps are you talking about? lambda calculus is one particular way to formalize program semantics, which is appropriate when talking about... program formalization

Lambda calculus is a thing that stays in colleges. Nobody uses it in the real world. Computers are imperative by design. Any community that tries to to apply some abstract theory to tools used in the real world is doomed to fail from the start.

Re: Compiling C to Safe Rust, Formalized

#166

[flagged]

Would you mind expanding on this? It sounds interesting, but I'm not tuned into either community enough to know what parallels you see.

Haskell philosophy is basically asumming that programmers were really bad at parallelism and thread saftey, and thus it was made to address this concern. However because that overarching idea is ideological in nature (i.e not true as a statement about programmers as a whole), the community was prevalent with ideology, using a lot of lambda calculus notation to set itself apart, and making coding in it cumbersome. As a result, nobody bothered to really do anything with it.

Rust has largely the same problem. You see bits of use of it here and there, but its also based in ideology that programmers are bad at managing memory.

From a technical viewpoint, Rust doesnt offer anything that doesnt already exist, while providing a more cumbersome way to code. Which is why its a days are numbered.

Re: Compiling C to Safe Rust, Formalized

#167

Earlier quoted context omitted.

With rust having recently entered the Linux kernel, Windows 11, qemu among others where Haskell never took a hold, I really fail to see where you feel the wind is blowing. The thing is, rust is used today in more and more places because it's reliable. We're not going to switch out the ground we are standing on every time something shiny comes along and that's why this is such an interesting development.

Even steel plated armour succumbs to rust given the environment and time

I clearly remeber seeing replies similar to yours from the Haskell fans:)

Re: Compiling C to Safe Rust, Formalized

#168

Earlier quoted context omitted.

Would you mind expanding on this? It sounds interesting, but I'm not tuned into either community enough to know what parallels you see.

Haskell philosophy is basically asumming that programmers were really bad at parallelism and thread saftey, and thus it was made to address this concern. However because that overarching idea is ideological in nature (i.e not true as a statement about programmers as a whole), the community was prevalent with ideology, using a lot of lambda calculus notation to set itself apart, and making coding in it cumbersome. As…

Haskell was most certainly not made to address a concern about programmers being really bad at parallelism and thread safety.

Re: Compiling C to Safe Rust, Formalized

#169
post #168

Earlier quoted context omitted.

Haskell philosophy is basically asumming that programmers were really bad at parallelism and thread saftey, and thus it was made to address this concern. However because that overarching idea is ideological in nature (i.e not true as a statement about programmers as a whole), the community was prevalent with ideology, using a lot of lambda calculus notation to set itself apart, and making coding in it cumbersome. As…

Haskell was most certainly not made to address a concern about programmers being really bad at parallelism and thread safety.

It absolutely has. The functional programming paradigm is designed specifically to describe a program withoilut side effects, so you can be sure that execution is deterministic (and thus scalable and parallelizable). There are no other advantages to functional programming.

Re: Compiling C to Safe Rust, Formalized

#170
post #146

Earlier quoted context omitted.

The answer is that it is not. It frustrates me more than it should, I admit, that people always mention Rust when they talk about safety, but never Ada / SPARK. You want formal verification? Use Ada / SPARK. It has been battle-tested. It has been used for critical systems for a really long time now. (And a compiler being formally verified vs. being able to write formally verified code means two different things.)

You also need to consider that formal verification is not the be-all/end-all of correctness. Formal verification is verifying a mathematical model of the program correct, according to certain mathematical correctness properties. That model may not actually represent the real world, or the correctness properties may not actually be the properties that you want to guarantee. Famously, there was the formally verified Ja…

The article talks about compiling formalized C code to Rust. While interesting from a tinkering perspective, I fail to see any significant utility in safety, security, readability, popularity and ease of language. Can you please educate me as to what I am missing
Post reply on HN