You know, there are other languages than Haskell doing interesting things. Ada2012 for example, introduced design by contract with support for formal verificati

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/projects/hi-lite/gnatprove/ http://www.open-do.org/wp-content/uploads/2011/12/hi-lite-erts2012.pdf http://www.open-do.org/wp-content/uploads/2011/12/hi-lite-er...