If you really have followed the research in type systems and see how it *factually* intersects with practical reality you wouldnt joke about it. Its a bizzare nonsense what they do in „research“ and sane implementations (only slightly grounded in formalisms) are actually used
I do, and hope that one day stuff like dependent types and formal proofs are every day tools, alongside our AI masters, which also don't use any learnings from scientific research.