You know, there are other languages than Haskell doing interesting things. Ada2012 for example, introduced design by contract with support for formal verification in conforming subprograms. This may be a near term more practical path than dependent types. Highly interesting.

-> http://www.open-do.org/projects/hi-lite/gnatprove/

http://www.open-do.org/wp-content/uploads/2011/12/hi-lite-er...