This one is beautiful as well. It was mind-opening for me to think of types in terms of provability (intuitionistic/constructive logic) rather than truth (clas

This one is beautiful as well. It was mind-opening for me to think of types in terms of provability (intuitionistic/constructive logic) rather than truth (classical logic). The only way to prove that a function returning a value of type T actually halts (and therefore does not actually “return” bottom/void) is to run it and obtain that T value, i.e., to find the object that the type claims exists.