> But, this isn't just about rewriting code from one language to another. It's about reverse engineering complex information out of the code, which may not be immediately visible in it, and then finding a way to make it "safe" according to Rust's type system. Where's the training data for that? It'd be really hard even for skilled humans.

That might not be too bad.

A combination of a formal system and an LLM might work here. Suppose we see a C function

   void somefn(char* buf, int n);

First question: is "buf" a pointer to an array, or a pointer to a single char? That can be answered by looking at what the function does with "buf", and what callers pass to it.

If it's an array, how big is it? We don't have enough info to know that yet. But a reasonable guess, and one than an LLM might make, is that the length of buf is "n".

Following that assumption, it's reasonable to translate this to Rust as

   fn somefn(buf: &[u8])

and, if n is needed within the function, use

   buf.len()

The next step is to validate that guess. The run-time approach is to write all calls to "somefn" with

   assert!(buf.len() == n);
   somefn(buf, n);

Maybe formal methods can prove the assert true, and we can take it out. Or if a SAT solver or a fuzz tester can generate a counterexample, we know that the guess was wrong and this has to be done the hard way, as

   fn somefn(buf: &[u8], int n)

implying more subscript checks inside "somefn".

The idea is to recognize common C idioms and do clean translations to Rust for them. This should handle a high percentage of cases.