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

111–120 of 173 posts

Re: Compiling C to Safe Rust, Formalized

#111

Post by medo-bear »

gpm wrote: post #110
medo-bear wrote: post #99

Earlier quoted context omitted.

What is the benefit of compiling formally correct code to Rust? It seems that all the possible benefits are already there (if not more)

I suppose hypothetically putting it in an easier language to make changes in. Though it's hard to imagine it being easier to make changes to transpiled code than the original. Alternatively this might be seen as a stepping stone to translating non-formally-verified C to rust, which I understand the US government has expressed a fair bit of interest in.

Good luck with both of that. Otherwise people whose dayjob is rewritting everything in Rust will soon be out of a job

Re: Compiling C to Safe Rust, Formalized

#112

Post by Ar-Curunir »

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…

Rust is stable and used by a number of big players, while Zig is not stable, and as a result hasn’t seen widespread adoption yet

Re: Compiling C to Safe Rust, Formalized

#113

Post by keybored »

johnisgood wrote: post #108
medo-bear wrote: post #107

Earlier quoted context omitted.

I think a disclaimer like this should be written with every Rust application, like health warnings on cigarette packets

At this point, I think that would be better, yes, just because people think Rust is "fully" safe, which is just incorrect. I think the problem was the Rust hype and repeated statements of it being very safe, so we have some undoing to do. For example if someone on GitHub sees that the project is written in Rust, they are automatically going to assume it is safe, incorrectly so. I do not blame them though.

You presumably extend this to every virtual machine or interpreter for every language which is implemented in an unsafe language. When that language claims to be safe (like all such languages claim to be).

That seems excessive and tedious.

Re: Compiling C to Safe Rust, Formalized

#114

Post by chillingeffect »

johnisgood wrote: post #108
medo-bear wrote: post #107

Earlier quoted context omitted.

I think a disclaimer like this should be written with every Rust application, like health warnings on cigarette packets

At this point, I think that would be better, yes, just because people think Rust is "fully" safe, which is just incorrect. I think the problem was the Rust hype and repeated statements of it being very safe, so we have some undoing to do. For example if someone on GitHub sees that the project is written in Rust, they are automatically going to assume it is safe, incorrectly so. I do not blame them though.

Rust is to safe as Tesla is to autopilot.

Re: Compiling C to Safe Rust, Formalized

#115

Post by medo-bear »

keybored wrote: post #113
johnisgood wrote: post #108

Earlier quoted context omitted.

At this point, I think that would be better, yes, just because people think Rust is "fully" safe, which is just incorrect. I think the problem was the Rust hype and repeated statements of it being very safe, so we have some undoing to do. For example if someone on GitHub sees that the project is written in Rust, they are automatically going to assume it is safe, incorrectly so. I do not blame them though.

You presumably extend this to every virtual machine or interpreter for every language which is implemented in an unsafe language. When that language claims to be safe (like all such languages claim to be). That seems excessive and tedious.

The point, I think, was that "safety" presumptions about Rust are often exaggerated or poorly misunderstood due to hype. That could certainly lead to problems

Re: Compiling C to Safe Rust, Formalized

#116

Post by medo-bear »

chillingeffect wrote: post #114
johnisgood wrote: post #108

Earlier quoted context omitted.

At this point, I think that would be better, yes, just because people think Rust is "fully" safe, which is just incorrect. I think the problem was the Rust hype and repeated statements of it being very safe, so we have some undoing to do. For example if someone on GitHub sees that the project is written in Rust, they are automatically going to assume it is safe, incorrectly so. I do not blame them though.

Rust is to safe as Tesla is to autopilot.

As Tesla is to Tesla

Re: Compiling C to Safe Rust, Formalized

#117

Post by glouwbug »

dhosek wrote: post #65
immibis wrote: post #57

Earlier quoted context omitted.

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

Given that in my (small, employer-mandated) explorations with Copilot autocompletions it’s offered incorrect suggestions about a third of the time and seems to like to also suggest deprecated APIs, I’m skeptical about the current generation’s ability to be useful at even this small task.

Sure but it takes two copilots to fly a plane

Re: Compiling C to Safe Rust, Formalized

#118

Post by glouwbug »

zxvkhkxvdvbdxz wrote: post #46
ActorNightly wrote: post #26

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

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

Re: Compiling C to Safe Rust, Formalized

#119

Post by woodruffw »

medo-bear wrote: post #115
keybored wrote: post #113

Earlier quoted context omitted.

You presumably extend this to every virtual machine or interpreter for every language which is implemented in an unsafe language. When that language claims to be safe (like all such languages claim to be). That seems excessive and tedious.

The point, I think, was that "safety" presumptions about Rust are often exaggerated or poorly misunderstood due to hype. That could certainly lead to problems

I don’t think Rust’s actual safety properties aren’t overhyped, although they may be subject to misunderstanding about their exact extent.

Concretely: spatial and temporal memory safety are good things, and Rust achieves both. It’s not unique in this regard, nor is it unique in not having a formal definition.

Re: Compiling C to Safe Rust, Formalized

#120

Post by nickpsecurity »

DonaldPShimoda wrote: post #69
nickpsecurity wrote: post #37

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

There’s tools that prove the safety of C code. They include RV-Match, Astree Analzer, and Frama-C. CompCert certifies the compilation. There’s tons of tools to find bugs by model checking, test generation, etc. Rust was nowhere near C last I checked in terms of tooling available.

So, back to my original comment, the investment in making a Rust to C transpiler would make a C to safer C transpiler that fed that code into the verification tooling. A small transpiler would be easier to write with huge, immediate gains.

On field proven, there’s two angles: spec and code. Many C/C++ apps didn’t become usable at all until years of iteration based on feedback from field use. An alternative in Rust might have incorrect specs which. From there, a number have had much code review, static analysis, and testing. They have few to no known bugs at any point. So, there are definitely C/C++ applications out there that are field-proven with a decent level of safety.

(Note: Any transpiler might need to be bug for bug and weird behavior for weird behavior compatible to match the implicit spec in the C/C++ code.)

You’re right about the average Rust vs C code, like type system vs correctness. I’d prefer new code be written in safer languages, which I added to my proposal.

If apples to apples on correctness, you’d have to compare C written for verification with Rust. Quite a few C projects have been proven to be correct. Since you’re using a compiler, I’ll add that tools like Softbound+CETS make C code safe automatically.

I do think Rust brings the cost and effort down quite a lot, though. It’s tooling is usually more mature or at least free than most for verifying C.

Post reply on HN