Did you know dep. type languages can have

mutable arrays? I didn't until today:

http://cs.ru.nl/~wouters/Publications/MoreDepTypesForDistrArrays.pdf

No out of bounds exceptions, and you can prove shit like the idempotence of a swap operation repeated twice on the same pair of array elements. Good stuff.

>>10
Because the whole idea is that types come first. Development is interactive, you write down your types and the IDE writes the implementation for you, with some holes that you fill. I.e. types define not only the specification of code, but also in a large part the implementation itself.