Depently typed my ass

Creating libraries for dependently typed languages is an interesting problem. I worked for a while on making a tree map (like Haskell's Data.Map) that took advantage of dependent types; for example, supplying proofs that a key either exists or does not in tree. There are oodles of things to compute and prove, it's not clear what a nice API would look like. For example, a proof that a key either exists or does not is a much larger data structure than a simple boolean true/false. I am really excited to see what these sorts of libraries will look like.

Decompilers make machine code human readable. The problem is that there is still no way to quickly ask IDE "Computer, what does this function do? Explain in a few english words."