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.

>>1

Does anyone really think that dependent types will ever lift off for practical programming?

No. The future belongs to the fuzzy pattern matching system. See http://www.cs.unc.edu/~jtighe/Papers/ECCV10/

Basically programmer would draw a diagram with some annotated arrows, where to place what and what to repeat, and then it would be translated into AST and evaluated, possibly preserving a level uncertainty where needed.

I.e. a diagram with a word "find" (or just a picture of magnifying glass) with an arrow pointing to an image of a cat (pasted from clipboard) and a another arrow pointing to a picture of a hard drive.