Your first point is of course true, but most statements about the behaviour of code needs to have "assuming no bugs" appended to it, so I'm not sure that it's a particularly interesting point. A more precise interpretation might be that the translator is likely to have more bugs than other components in the pipeline (the compilers and linkers etc.), since it is unlikely to be used nearly as much as them; I wonder if one could do things like compile with rustc and clang and somehow compare the LLVM IR for equivalence (but... I suspect that the code generation patterns for each aren't similar enough).

As for unspecified behaviour... that's true! Again I wonder if clang is a useful component here: I suspect if C code behaves correctly with clang, then the translation to Rust compiled with rustc probably works too, both because the translator uses clang, and because both compilers use LLVM.

The point (in contrast to the usual complaint of Animats) I was trying to convey, but was nitpicked was: a correct translation from fully-specified C to unsafe Rust doesn't add any unsafety. Whether this applies in practice is slightly different, but there's questions about whether pretty much any statement about C code applies in practice: since undefined behaviour is so rife and easy to trigger, many/most programs are outside the specification (fuzzing C programs often results in segfaults---undefined behaviour---and so the program is outside the bounds of C).

Wrapping up, I'll emphasise that the value in this sort of translation is as a stepping stone towards safe Rust, not as a final `unsafe` product.