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.