I think Jacques possibly means the ability to do static checking of matrix and vector extents, to make sure that you don't try to perform operations like matrix-vector multiply on operands whose extents do not match. If you want to have this ability on your language, then you will have to restrict the way you are allowed to construct array bounds so the equations that arise can be solved. Possibly a dependent type system can be helpful for this.
This is indeed what I meant. If one is going to move from a dynamically typed language (like Matlab, Maple, Mathematica, etc) to something statically typed, then the expectation is that this is going to truly help. And, for many applications, it does [this is partly why I have an MSc student coding a reverse engineering application in Haskell]. Since the claim of static typing is that things cannot go wrong at run-time, one start to think (incorrectly, but optimistically) that this means that 'nonsense' cannot happen at run-time. And multiplying matricies with non-matching sizes is nonsense, so it is rather disappointing that, without tricks, this is not caught at compilation time. Matrix length are one of many commonly occuring dependent types in mathematics. Variable names for polynomials, expansion point and 'scale' for generalized series expansions, coefficient ring for normalization and factorization of polynomials, and so on up the food chain. The dependencies get quite interesting when one is dealing with modelling mixed PDEs and recurrence equations as ideals in rings of Ore polynomials! Jacques