alt Hacker NewsIt's because you're not using words in the way that people use them when talking about this stuff.
Rust (outside of the unsafe superset) has no undefined behavior. That is guaranteed, statically, at compile time: all execution paths have well-defined behaviors. That does not mean that there are no runtime consequences whatsoever. For example, the behavior of an invalid index is a panic, at runtime. Inserting a check for an invalid index at compile time is static enforcement of the behavior, even if the check itself happens at runtime.
If you had said "sometimes, Rust can't eliminate dynamic checks because it doesn't have a strong enough reasoning about some compile time properties" nobody would be arguing with you about this. Your example is one where a language with stronger reasoning would be able to detect it, for sure. Lean can do this, for example.
Rust does not do prevent all UB statically. Even if you guarantee at compile-time that all execution paths have well-defined semantics because compiler inserted run-time checks, this is not the same thing as "statically ensuring the absence of this run-time condition that would cause UB" which would be what people usually mean with "statically preventing UB". So I think it is not me who uses the works in an unusual way.
If, of course, you redefined words so that adding run-time checks counts as "statically preventing all UB", then this applies to Fil-C just as well! You can not have it both ways.