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.

>>9
Every time I see dependent typing enthusiasts prattling about their languages, they're talking about the types themselves. I don't see anyone talking about building software in these languages. It's suspiciously exactly the same as the OOP hype back when that was a thing.