54 ms·

a) if every C program could be translated into an equivalent safe Rust program, that would mean that each C program is as safe as the safe Rust equivalent. b) s

a) if every C program could be translated into an equivalent safe Rust program, that would mean that each C program is as safe as the safe Rust equivalent. b) since there are C programs that are open to memory currption in a way safe Rust isn't, this corruptability would need to be translated into partially unsafe Rust. Congrats, you now have a corruptible Rust program, what's the point again?? c) so DARPA must be trying to fix/change what the program is doing when switching to Rust. So how to discern what behaviour is intended and which is not? Doesn't this run directly into the undecidability/uncomputability of the halting problem!?!

Arnavion 2y ago
>Doesn't this run directly into the undecidability/uncomputability of the halting problem!?! The programmer gets to decide. DARPA does not expect the translator program to autonomously output a perfect Rust program. It just wants a "high degree of automation towards translating legacy C to Rust" (from the sam.gov link in the submission, emphasis mine).
im3w1l 2y ago
Memory corruption is undefined behavior and means the compiler is free to do anything it wants. Anything it wants... and that includes doing something entirely safe and reasonable. If you write out of bounds, the compiler is allowed to shut the program down in a controlled manner. It's allowed to transparently resize the array for you. Etc. Hence a rust translation can do these things.
- fch42 2y ago
  You "anything it wants" folks really annoy me a little. If the compiler can, compile-time, detect that code is prone to memory corruption, it can warn the developer. If it can't detect it at compile time, will and shall it add some sort of magic signal handler heuristic to determine whether a segfault occurred due to a runtime-provable specific instance of memory corruption and hence format your harddrive, while for runtime-indeterminable kinds it'd rather fry cpu core seven preemptively ? But that behaviour changes in the next version to blink sos on the network cable leds ? I mean, it were cool if compilers used their "freedom" here to output nagging messages "the mem-safe UB brigade told you so, told you so, told you so ...". The fact they don't tells me, at least, that compiler developers follow Postel's law - be strict at what you emit but lenient at what you process. They're reasonable people. Not some sort of crusader out there to get you in the most excruciatingly painful ways. Undefined behaviour isn't unreasonable behaviour.
  - im3w1l 2y ago
    I think you misunderstand my point. Consider the following program: #include <stdio.h> int main(void) { int a[10]; a[20] = 100; printf("%d\n", a[20]); } because accessing a[20] is undefined behavior, it is legal to translate the program to the following rust code (which crashes with out of bounds error message during runtime). #![allow(unconditional_panic)] fn main() { let mut a: [i32; 10] = [0; 10]; a[20] = 100; println!("{}", a[20]); } It gives a different result than gcc. But one that is both valid one and useful. And that's why machine-translating to rust could have benefits in practice. Contrary to simon_void's assertion, you can translate a corruptible program to a non-corruptible one. (In this particular case the error is simple enough that the compiler catches it and we have to tell it to go ahead anyway, but in more complicated cases it wont be. So please don't get hung up on this point)

Arnavion 2y ago

>Doesn't this run directly into the undecidability/uncomputability of the halting problem!?! The programmer gets to decide. DARPA does not expect the translator program to autonomously output a perfect Rust program. It just wants a "high degree of automation towards translating legacy C to Rust" (from the sam.gov link in the submission, emphasis mine).

im3w1l 2y ago

Memory corruption is undefined behavior and means the compiler is free to do anything it wants. Anything it wants... and that includes doing something entirely safe and reasonable. If you write out of bounds, the compiler is allowed to shut the program down in a controlled manner. It's allowed to transparently resize the array for you. Etc. Hence a rust translation can do these things.

fch42 2y ago
You "anything it wants" folks really annoy me a little. If the compiler can, compile-time, detect that code is prone to memory corruption, it can warn the developer. If it can't detect it at compile time, will and shall it add some sort of magic signal handler heuristic to determine whether a segfault occurred due to a runtime-provable specific instance of memory corruption and hence format your harddrive, while for runtime-indeterminable kinds it'd rather fry cpu core seven preemptively ? But that behaviour changes in the next version to blink sos on the network cable leds ? I mean, it were cool if compilers used their "freedom" here to output nagging messages "the mem-safe UB brigade told you so, told you so, told you so ...". The fact they don't tells me, at least, that compiler developers follow Postel's law - be strict at what you emit but lenient at what you process. They're reasonable people. Not some sort of crusader out there to get you in the most excruciatingly painful ways. Undefined behaviour isn't unreasonable behaviour.
- im3w1l 2y ago
  I think you misunderstand my point. Consider the following program: #include <stdio.h> int main(void) { int a[10]; a[20] = 100; printf("%d\n", a[20]); } because accessing a[20] is undefined behavior, it is legal to translate the program to the following rust code (which crashes with out of bounds error message during runtime). #![allow(unconditional_panic)] fn main() { let mut a: [i32; 10] = [0; 10]; a[20] = 100; println!("{}", a[20]); } It gives a different result than gcc. But one that is both valid one and useful. And that's why machine-translating to rust could have benefits in practice. Contrary to simon_void's assertion, you can translate a corruptible program to a non-corruptible one. (In this particular case the error is simple enough that the compiler catches it and we have to tell it to go ahead anyway, but in more complicated cases it wont be. So please don't get hung up on this point)