It seems easy (relatively speaking) to directly translate C to Rust if you're allowed to use unsafe and don't make an effort to actually verify the soundness of

It seems easy (relatively speaking) to directly translate C to Rust if you're allowed to use unsafe and don't make an effort to actually verify the soundness of the code. But if you need to verify the soundness and fix bugs while translating it? That's really hard, and that's what it sounds like what TRACTOR wants to do. Using "unsafe" doesn't automatically make Rust useless, of course, but the example on the c2rust website itself doesn't make any effort to verify its usage of unsafe (you can easily read memory out of bounds just by changing "n" to "n + 1" in the example loop). Sadly, that is a much, much harder problem to solve even for fairly basic C programs.