I think you misunderstand my point. Consider the following program: #include <stdio.h> int main(void) { int a[10]; a[20] = 100;

I think you misunderstand my point. Consider the following program: #include <stdio.h> int main(void) { int a[10]; a[20] = 100; printf("%d\n", a[20]); } because accessing a[20] is undefined behavior, it is legal to translate the program to the following rust code (which crashes with out of bounds error message during runtime). #![allow(unconditional_panic)] fn main() { let mut a: [i32; 10] = [0; 10]; a[20] = 100; println!("{}", a[20]); } It gives a different result than gcc. But one that is both valid one and useful. And that's why machine-translating to rust could have benefits in practice. Contrary to simon_void's assertion, you can translate a corruptible program to a non-corruptible one. (In this particular case the error is simple enough that the compiler catches it and we have to tell it to go ahead anyway, but in more complicated cases it wont be. So please don't get hung up on this point)