That assumes that such a translation is either a binary success/failure, runs at once, and runs for the entire kernel. More likely, such a tool will be used fi

That assumes that such a translation is either a binary success/failure, runs at once, and runs for the entire kernel. More likely, such a tool will be used file-by-file and module-by-module, and when it fails, it will either report obvious mistakes (that will then be fixed in the C source, in the same way that e.g. people doing Python 2 to 3 conversions end up fixing bugs in their Python 2 code to prepare it for reliable conversion) or report more complex design mistakes that warrant rethinking an approach from scratch and starting the new implementation in Rust. If that's what happens, then we would not be proving the Linux kernel safe, and we would have a strong argument for having done the translation.