What I was (badly) trying to express was more that given static bounds rust could also eliminate dynamic checks. So saying e.g. ATS can eliminate static checks, is kind of switching the target.

https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML... is the kind of thing I mean - ATS programs can include proofs that an array access will be safely within bounds, even if we don't have an exact literal subscript in the code.