Dependent types FTW

http://www.cse.chalmers.se/~nad/listings/dependent-lenses/README.html#1

Good thing they've provided dependent lenses side by side with non-dependent. Cause the dependent version is like 10 fucking times longer. Does anyone really think that dependent types will ever lift off for practical programming? I think that would require fucking autogeneration of proofs but that would make a human programmer obsolete.

All this thread tells me is that programming is being dumbed down and autists with no talent want everything to be automated for what purpose? Money. And to do what with it? Nothing but live pathetic, meaningless lives.