Yes, it's pretty much impossible to prove anything about arbitrary programs.

However if you are willing to restrict what programs you allow, you can make guarantees possible.

Silly example: if you compile valid (safe) Rust programs to C, you know that the resulting code will not invalidate Rust's borrowing rules by construction; and in principle you could try to establish this guarantee just from the C code alone, never having seen the Rust original.

However, you still wouldn't be able to have an algorithm that tells you for any arbitrary C code whether it has these problems or not.

> if you compile valid (safe) Rust programs to C, you know that the resulting code will not invalidate Rust's borrowing rules

If you know the compiler is correct, which you don't.