@clacke This is why I think the formal methods industry and research communities have it all wrong. They should not be looking to make their systems tighter (this is always a good thing to do regardless), but rather they need to be making their contributions more approachable to knuckle-dragging grunts in the field like me.
R&D into type systems falls into this latter category, which is why Haskell monads and Rust's ownership ideas are ground-breaking. We need more of *this*, and less of Z.