It'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.

These are all true? I don’t see the problem?

Rust does prefer static checks. It uses static analysis to prevent many types of bugs - including use-after-free and data races. But you’re right; rust still falls back to runtime checks when static analysis is too hard. Like dynamic bounds checking and integer overflow (in debug mode). Cell, Refcell and friends also have a (small) runtime cost. Rust prefers static analysis but does not use it exclusively.

Let’s say rust is 80% static analysis, 20% dynamic checks. Fil-C seems to go the other way and have 80+% dynamic checks. It’s an interesting point.

Nobody disagrees with you that rust sometimes inserts dynamic bounds checks. But “prefer” in this context means “most of the time, when possible” not “all of the time”. I prefer vanilla ice cream over chocolate. But I still eat chocolate ice cream when vanilla isn’t available. Pointing out that one time I ate chocolate ice cream isn’t a gotcha moment.