I mean, if it compiles it typechecks is kind of tautological, and not particularly effective as a saying or slogan. I feel like you miss the point of a phrase like that, which like any aphorism, slogan, saying, or rule of thumb is not about representing reality with 100% accuracy but instead about conveying an idea.

The only two languages I’ve worked with that gave me the feeling that I could generally trust a compiling program to be approximately correct are Rust and Haskell. That difference relative to other languages is meaningful enough in practice that it seems to me to be worth a slogan. I believe it’s meant to be more of a “works, relative to what you might expect from other languages” kind of thing versus, “is a completely perfect program.”

And, if you care about maximizing the “if it compiles it works” feeling, it’s possible to use .get() for array access, to put as much logic in the type system as is feasible, etc. This is probably more idiomatic and is generally how I write code, so it does often feel that way to me, regardless of whether it is completely, objectively, literally true.