The reason why Rust and other languages have bounds checking that approaches C’s speed is less to do with the compiler being able to prove away bounds checks and more to do with those languages making the bounds easy to carry around.

Bounds checks themselves aren’t that expensive, if you already have the length to check against in a register or some other convenient spot.

And - if the bounds are convenient to find and known to be immutable then it does make it easier for the compiler to eliminate those checks using the same techniques it would use to eliminate all kinds of redundancies. C has many redundancies that we don’t have to think about because they’re straightforward for the compiler to reason about.