To apply a formal method to your work requires to acknowledge that your intuition might me wrong, your past decisions incorrect, and your knowledge of the subject area deficient. Often you have to step back, rethink, and rework.
This is a normal mindset for a scientist, and a pretty common mindset for an experienced engineer.
But this view is not automatically acquired with an engineering diploma, with obvious coding skills, or even with a couple successful open-source projects. It has to be nurtured consciously—or rammed down your throat by unforgiving reality; the latter is pretty traumatic.
When one is a polyglot developer, we are like mercenaries, a bag full of tools, each with its caveats, and we care about the solution less how we got there juggling those tools.
Developer X tend to keep searching for external confirmation that they did the right choice. Any attack on tool X triggers defensive attacks, as if they would be a personal attack.
Of course I am exaggerating here, just extrapolating from those that I know on my circle.
It's pretty dramatic so it gets met with preemptive defensiveness.
From the end of article: Everything is broken. Everything is fine.
In practice, there are ranges of brokenness. If you have to go hunting for the problem, and it takes a combination of 5 obscure features which nobody would ever use together, it's not that big a deal. If it's the sort of thing that you encounter in any non-trivial program, well....
... your language dies.
Part of the reason so many people in this thread can be cavalier about type soundness issues is precisely that all the languages they use, being the languages that did not die because they have a crappy type system, are pretty sound, within the model the language is operating under, so, yeah, of course it doesn't look like a problem to a normal programmer, because it was solved a long time ago. Doesn't mean it's a bad idea, or that people should just sneer contemptuously at the issues and snidely dismiss them as academic frippery, because then these people go on to write new languages that have these sorts of issues.
(Like the recent wave of "event based" programming environments that just threw away the benefits of structured programming, because they were so thoroughly immersed in a structured programming world they didn't even realize how thoroughly they'd internalized it, had no idea what the preconditions were for it, and not only had no idea they were throwing it away but snidely berated people who pointed it out. And then spent 5+ years rediscovering it all over again....)
HN is less prone to toxicity, but this is reminiscent of Reddit and it drives away the people that want to help.
As a piece of advice, some type theory never harmed anyone ;-)