Comment by 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