[zem]

ATS could probably do some of this by constructing proofs about the bounds and indices - not in the completely general case of course, but for at least some fraction of what a language without dependent types would have to defer to runtime

[ratmice]

those are not dynamic bounds.

[LoganDark]

All "dynamic" means is that you don't know or don't prove the precise value statically. However you may know the range of possible values, or you may know properties of your algorithm that mean it can never attempt an out-of-bounds access. Sometimes you don't know any of these things, but sometimes you do.

[ratmice]

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.

[zem]

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.