Somewhat related: What has blown my mind at some point is that with dependent types you can actually check your algorithms for correctness. --- Example: http:

Somewhat related: What has blown my mind at some point is that with dependent types you can actually check your algorithms for correctness. --- Example: http://goto.ucsd.edu:8090/index.html#?demo=Order.hs http://goto.ucsd.edu:8090/index.html#?demo=Order.hs Press Check -> The button should turn green and say "Safe" Now mess up the algorithm, e.g. change the `>=` in line 174 to `<=` in effect changing the sorting order. Press Check again -> The button should turn red and the line you changed should be highlighted telling you that at this point you violated the ordering constraint that put in place by the `IncrList a` type. --- To be fair, I don't think too many programming work is low-level algorithmic programming where this would be applicable. I see the benefits in having type level size constraints on arrays or having a "Safe / Unsafe" constraint on input from users that can only be changed by running through verification functions.