What is Expressiveness in a Computer Language

[Benjamin Franksen]

Specialized
language already exist that reliably (as in, all the time) move array
bounds checking to compile time;

It sounds like this means the programmer has to code up what it means to
index off an array, yes? Otherwise, I can't imagine how it would work.

x := read_integer_from_stdin();
write_to_stdout(myarray[x]);

What does the programmer have to do to implement this semantic in the
sort of language you're talking about? Surely something somewhere along
the line has to "fail" (for some meaning of failure) at run-time, yes?

You should really take a look at Epigram. One of its main features is that
it makes it possible not only to statically /check/ invariants, but also
to /establish/ them.

In your example, of course the program has to check the integer at runtime.
However, in a dependent type system, the type of the value returned from
the check-function can very well indicate whether it passed the test (i.e.
being a valid index for myarray) or not.

Ben