Decouple the actions

Posted Aug 20, 2024 15:29 UTC (Tue) by roc (subscriber, #30627)
In reply to: Decouple the actions by Vorpal
Parent article: FreeBSD considers Rust in the base system

If the LLM produces Rust code *and* a formal proof that the Rust code is equivalent to the input C code, then it's very easily decidable whether the proof is valid.

That's a big "if" of course. No-one's saying this is easy or even actually feasible. This is research.

Decouple the actions

Posted Aug 20, 2024 16:02 UTC (Tue) by leromarinvit (subscriber, #56850) [Link] (2 responses)

If you can prove that any safe Rust program is equivalent to a given C program, that means the C program can't have any memory safety issues to begin with. How many large C code bases (the ones you'd want to convert to Rust) are there for which this can be said with any reasonable certainty?

If you have such a (memory safety) bug-free C program, then yes, you could use the Rust code generated by such a hypothetical converter to make introducing bugs in the future harder. But if you want to convert to Rust to weed out existing, uncaught issues, doesn't demanding a formal proof of equivalence make the problem literally impossible to solve?

Decouple the actions

Posted Aug 21, 2024 11:52 UTC (Wed) by roc (subscriber, #30627) [Link] (1 responses)

> If you can prove that any safe Rust program is equivalent to a given C program, that means the C program can't have any memory safety issues to begin with. How many large C code bases (the ones you'd want to convert to Rust) are there for which this can be said with any reasonable certainty?

It's more nuanced than that because you can refine the notion of "equivalent". You could, for example, use "equivalent, assuming that the C program never triggers undefined behavior" (i.e. the notion of equivalence that C compilers use when applying optimizations).

Or you could analyze the complete system and prove that for all the cases that can happen in practice, some C function is equivalent to some Rust function, even though in a different context it might behave differently and do something unsafe.

Definition of "equivalent" for TRACTOR

Posted Aug 21, 2024 12:40 UTC (Wed) by farnz (subscriber, #17727) [Link]

And one of the reasons that TRACTOR is a research proposal, and not something that "just" needs implementation work, is that the definition of "equivalent" that DARPA are aiming for is "what a Rust programmer would write, given the same specification that caused a C programmer to write this C code".

So, assuming DARPA fund a research team to see where they get to from here, part of the project will be to define what "equivalent" actually means - there will be some things that are technically UB where TRACTOR is expected to work out that a human programmer would expect it to be meaningful (and what that meaning is), for example.

The TRACTOR project as a whole is not a small idea - it's a big and far-reaching project that's likely to come up with a negative result - "this can't be done usefully because" - but where if it does come up with a positive result - "here is a machine that gets you all the way from a typical C codebase to a high quality Rust codebase, ready for a Rust programmer to refactor" - it's a huge deal.