This is wonderful. I feel myself thoroughly agreeing (but also somehow intensely disagreeing at the same time) with things that are written, especially when it comes to type systems. At some sort of deep level, I seem to like the idea that stuff is proven to work, regardless of how complex the type system overhead is. Maybe it's just two sides of the same coin. Some sort of primitive hatred of complexity and a primitive desire for safety and control will forever be at war inside me.