Remember that a string is a kind of array, and inherits all of the same properties.
Languages such as Rust that lean on inference are an absolute joy to program in.
That said, there's the solution: type level integers.
(That also said, Rust's String type isn't an array, because it's mutable, so the size can't be a part of the type)
I wouldn't say it's production quality yet... But it's a work in progress, and achieves far more than you are requesting here.
I still think liquid haskell is too immature (Integer is not a good theory for Int, type classes aren't handled well, etc), but the promise is fascinating if the issues get worked out.
Even Java has a sane typing system if you stay away from arrays (use ArrayList for crying out loud) but beyond Java, there is a wealth of languages with very good static type systems (Scala, Kotlin, Ceylon).
Division by zero is passe; we just define a type that excludes zero, and make the division operator's denominator of that type.