Ada arrays are actual types, they're bounds-checked, the language provides some niceties for indexing, and Ravenscar and SPARK are available. You're going to have less issues with Ada in that case than you are with just about any other language out there.