Live data from Hacker News

Translating All C to Rust (TRACTOR)

darpa.mil

151–160 of 403 posts

Re: Translating All C to Rust (TRACTOR)

#151
post #144

Earlier quoted context omitted.

> or written in "safe" languages So when those languages have 'unsafe' constructs what are the rules going to be around using those? Without a defining set of rules to use here you're just going to end up right back where you started. > to migrate to safe languages, which Rust is an example of Rust has a safe mode. It is _not_ a safe language. To do anything interesting you will require unsafe blocks. This will not g…

> To do anything interesting you will require unsafe blocks. This will not get you very much. This is not true.

> This is not true.

Burying unsafe blocks in unevaluated cargo modules does not make this true. You're just taking the original problem and sweeping it under the rug.

Re: Translating All C to Rust (TRACTOR)

#152

That sounds ... hard. Especially as idiomatic Rust as written by skilled programmers looks nothing like C, and most interesting code is written in C++ anyway. Isn't it equivalent to statically determining the lifetimes of all allocations in the C program, including those that are implemented using custom allocators or which cross into proprietary libraries? There's been a lot of research into this sort of thing over…

I have to imagine that in the general case it will be a translation to unsafe Rust, with occasional isolated leaf nodes being translated to safe Rust. If you think it's hard wrestling with the borrow checker, just imagine how much harder it is to write automatic translation to borrow-checker-approved code that accounts for all the possible program space of C and all it's celebrated undefined behavior. A classic probl…

> have to imagine that in the general case it will be a translation to unsafe Rust, with occasional isolated leaf nodes being translated to safe Rust.

That’s not what they are aiming for. FTA: “The goal is to achieve the same quality and style that a skilled Rust developer would produce”

> just imagine how much harder it is to write automatic translation to borrow-checker-approved code that accounts for all the possible program space of C and all it's celebrated undefined behavior

Nitpick: undefined behavior gives the compiler leeway in deciding what a program does, so the more undefined behavior a C program invokes, the easier it is to translate its code to rust.

(Doing that translation in such a way that the behavior remains what gcc, clang or “most C compilers” do may be harder, but I’m not sure of that)

Re: Translating All C to Rust (TRACTOR)

#153

Earlier quoted context omitted.

> I think a far better and more mature process is to update C to modern C and use a model checker such as CBMC to verify memory, resource, and integer math safety. No chance. CBMC is amazing, but have you actually tried formally verifying a "real" program? I agree replacing with a hand-architected Rust version is clearly the better solution but also more expensive. I think they're going for an RLBox style "improve se…

> No chance. CBMC is amazing, but have you actually tried formally verifying a "real" program? Yes. Every day. It's actually quite easy to do. Write shadow methods covering the resources and function contracts of called functions, then verify the function. Repeat all of the way up and down the stack. It adds about 30% overhead over just TDD development.

Last time I tried CBMC, it ended up running out of memory for relatively small programs, do you encounter any resource usage issues with it? I'm learning Frama-C and I find it more predictable, although the non-determinism of solvers shocked me when I first tried to prove non-trivial programs. I guess ideally I would like something even more explicit than Frama-C.

Re: Translating All C to Rust (TRACTOR)

#154

Earlier quoted context omitted.

It's very hard; DARPA likes to fund hard things[1] :-). This isn't, however, DARPA's first foray into automatic program translation, or even automatic translation into Rust[2]. [1]: https://www.urbandictionary.com/define.php?term=DARPA%20hard [2]: https://c2rust.com/

in this case it seems to me the hard task that DARPA has chosen is to get me to forget how much they spent on pushing Ada.

in this case it seems to me the hard task that DARPA has chosen is to get me to forget how much they spent on pushing Ada.

You hate jumbo jets, high-speed trains, air traffic control, and satellites?

Re: Translating All C to Rust (TRACTOR)

#155
post #91

It's good to see DARPA pushing on this. It's a hard problem, but by no means impossible. Translating to safe Rust, though, is going to be really tough. There's a C to Rust translator now, but what comes out is horrible Rust, which just rewrites C pointer manipulation as unsafe Rust struct manipulation. The result is less maintainable than the original. So what would it take to actually do this right? The two big prob…

I once tried to use c2rust as a starting point for rustification of code and... it's not even good at that. The code is just too freakishly literal to the original C semantics that you can't even take the non-pointery bits and strip off the unsafe block and use that as a basis. (To give you a sense, it translates something like a + 1 to a.unwrapped_add(1i32), and my recollection is that for (int i = 0; i In general,…

That doesn't mention the affine type problem. Rust references are restricted to single ownership. If A has a reference to B, B can't have a reference to A. Bi-directional references are not only a common idiom in C, they're an inherent part of C++ objects.

Rust has to use reference counts in such situations. You have an Rc wrapped around structs, sometimes a RefCell, and .borrow() calls that panic when you have a conflict. C code translates badly into that kind of structure.

Static analysis might help find .borrow() and .borrow_mut() calls that will panic, or which won't panic. It's very similar to finding lock deadlocks of the type where one thread locks the same lock twice.

(If static analysis shows that no .borrow() or .borrow_mut() for an RwLock will panic, you don't really need the RwLock. That's worth pursuing as a way to allow Rust to have back references.)

Re: Translating All C to Rust (TRACTOR)

#156

Earlier quoted context omitted.

DARPA is basically a state-sponsored VC that optimizes for completely different things. Instead of looking for 100x financial returns, they want technical advantages for the United States. The "moat" is the hardness of developing and operationalizing those technologies first.

DARPA's commercialization track record is decidedly mixed, so the VC comparison is unexpectedly apt :-) (But yes: DARPA's mandate is explicitly to discover and develop the next generation of emerging technologies for military use.)

> DARPA's commercialization track record is decidedly mixed...

If you count my number of attempts, sure.

If you count by impact, it's hard to come up with many things more impactful than the Internet...?

Re: Translating All C to Rust (TRACTOR)

#157

Earlier quoted context omitted.

It's very hard; DARPA likes to fund hard things[1] :-). This isn't, however, DARPA's first foray into automatic program translation, or even automatic translation into Rust[2]. [1]: https://www.urbandictionary.com/define.php?term=DARPA%20hard [2]: https://c2rust.com/

in this case it seems to me the hard task that DARPA has chosen is to get me to forget how much they spent on pushing Ada.

ada does not require 'pushing'.

once the maturity of the users advances to a sufficient point, then ada is the only solution.

"ada. used in creating reliable software since 1983"

when i first saw ada, i didn't understand the why. now i understand the why, but ada is effectively gone.

-- old fortran / C / Assembly programmer

Re: Translating All C to Rust (TRACTOR)

#158
post #140
post #47

Earlier quoted context omitted.

> today cars drive themselves You can attach about a hundred asterisks to that. If anything, I think self the failure to hit L5 driving after billions of dollars and millions of man hours invested is probably reflective of how automatic C to Rust translation will go. We'll cruise 90% of the way, but the last 10% will prove insurmountable with current technology. Think about the number of C programs in the wild that r…

This is the exact formulation of the argument before computers beat humans at chess, or drew pictures, or represented color correctly, or... Self driving cars will be solved. There is at least one general purpose computer that can solve it already (a human brain), so of a purpose built computer can also be made to solve it. In 10 (or 2 or 50 or X) years when Chevy, Ford, and others are rolling out cheap self driving…

> These problems really aren't analogous.

I'd put money on the solutions to said problems looking largely the same though - big ass machine learning models.

My prediction is that a tool like copilot (but specialized to this domain) will do the bulk of source code conversions, with a really smart human coming behind to validate.

Re: Translating All C to Rust (TRACTOR)

#159

Earlier quoted context omitted.

in this case it seems to me the hard task that DARPA has chosen is to get me to forget how much they spent on pushing Ada.

in this case it seems to me the hard task that DARPA has chosen is to get me to forget how much they spent on pushing Ada. You hate jumbo jets, high-speed trains, air traffic control, and satellites?

Do you know what fear is? Getting in an airplane where the flight controls use NPM.

Re: Translating All C to Rust (TRACTOR)

#160

Earlier quoted context omitted.

DARPA's commercialization track record is decidedly mixed, so the VC comparison is unexpectedly apt :-) (But yes: DARPA's mandate is explicitly to discover and develop the next generation of emerging technologies for military use.)

> DARPA's commercialization track record is decidedly mixed... If you count my number of attempts, sure. If you count by impact, it's hard to come up with many things more impactful than the Internet...?

Yeah, I meant by number. But also: ARPA didn't commercialize the Internet! They explicitly refused to commercialize it; commercialization only happened after an Act of Congress induced interconnections between NSFNET and commercial networks.
Post reply on HN