I struggle to believe that subscript checking can be automatically removed in arbitrary code in any language (at least, not without full dependent typing), e.g.

I struggle to believe that subscript checking can be automatically removed in arbitrary code in any language (at least, not without full dependent typing), e.g. it seems pretty hard to make guarantees about something like x[y[i]] with arbitrary y.