Comment by rtpg
11 years ago
I would like to point out that things like SQL injection are pretty easy to avoid by just typing(in the type theory sense) things out in a DSL properly, and not having straight string injection. You don't need crazy dependent types to employ the "make sure strings are escaped" strategies.
Infinite loops, on the other hand...
I'm pretty sure you can build a total language and outlaw infinite loops even without dependent types. It also turns out that you can basically do whatever you want in a total language with a good runtime so long as it does coinduction well.
I just think the only real motivation people have taken up on for total languages is their proof theoretic properties which drives you quickly to dependent types.
Sure, I'm pretty sure Turner's original Total Functional Programming proposal https://uf-ias-2012.wikispaces.com/file/view/turner.pdf doesdn't use dependent types, but I'm not sure it has what you mean by "a good runtime [that] does coinduction well".
All I mean by that is that you probably want to be able to evaluate a partiality monad in the runtime if you want to write an interpreter or webserver perhaps.