You can retreat to your corner of theory if you wish, I'll actually build stuff. The real world has scary things like malicious actors that will send payloads designed to break your system through side channels like timing and cosmic rays that can flip bits on your disk and erase the guarantees that you believed you had in your type system.

You are being needlessly antagonistic. On HN of all places we should know that research in type theory isn't purely academic navel gazing.

Isn't it great that we have both theory and practice and both impact each other? Makes our profession so much more fun! :)