What is Expressiveness in a Computer Language

[Benjamin Franksen]

George Neuner wrote:
> The point is really that the checks that prevent these things

[such as 'array index out of bounds']

> must be 
> performed at runtime and can't be prevented by any practical type
> analysis performed at compile time.  I'm not a type theorist but my
> opinion is that a static type system that could, a priori, prevent the
> problem is impossible.

It is not impossible. Dependent type systems can -- in principle -- do all
such things. Take a look at Epigram (http://www.e-pig.org/).

Systems based on dependent types such as Epigram are not yet mature enough
to be used for serious programming. However, they clearly show that these
things /are/ possible.

Cheers
Ben