If the transpilation itself is bug-free, why not? For static guarantees, provided we transpile Rust code that already compiles on a normal Rust compiler, the guarantees are already checked and there, and the dynamic ones such as bounds checking can be implemented runtime in C with no problems.
this assumes the rusty guarantees are transitive. There's no reason to believe it isn't, but it'd be nice to see some sort of proof, or at least an argument for it.
Borrow checker, and more generally any type checkers, are essentially terminating programs ran during compilation process, thus safety guarantees given by them are ensured before the code is transformed into some target language.
If you mean 'no bugs in compiler' then yes. The safety of the target language doesn't matter: the output C is has an equivalent role to output machine code, those languages themselves are as unsafe as they can get, it's just that compilers output is a safer subsection of 'all programs which can be expressed in them'.
That's a problem for almost every language, not just Rust. C++ also compiles to intermediate representations, and then to machine code. Errors happen on that path. Rust just get rid of a lot of errors that could have been in the original specification (the source code).
Rust does not generate machine code itself. It uses LLVM to do that and there is no proof that the transformations done by that continue to keep the borrow checker guarantees. One just assumes with sufficient testing all bugs will be discovered.
Then the machine code generated by LLVM is not run directly by modern CPUs and is translated into internal representation first. And the future CPUs will behave like JIT-compilers with even more complex transformations.
The intermediate C code generated by this project just adds yet another transformation not fundamentally different from any of the above.
Rust does not guarantee that all bounds checks can be proven correct at compile time, so it relies on runtime bounds checks. If this does not implement the same bounds checks, then probably not.
