Without a bunch of people doing basic research none of us would have jobs.
But coming down from the ivory tower of academia , do you really need to go to the trouble of writing your custom CMS in Haskell after proving it's correctness in Coq ?
As a further example , the succesful company KissMetrics built the first version of it's product in a month and shipped using SQLite (!!) as a DB.
In their own words , they optimized 100 % for shipping speed.
Software doesn't exist in a vacuum , it plugs into a business.
The amount of rigor and research that must go into a piece of software depends on the domain and business requirements. To insist that all software be written to such a high standard is unrealistic and will never happen.
I'm yet another software engineer who (most of the time) writes CRUD apps as quickly as possible so my boss pays me on time. I have no pretensions of being a 10x or being the hero who drags the world out of the dark pits of poorly specified and mathematically inelegant software with his superior intellect.
Also, it's fine to write a prototype to get to market faster. But building further on top of that prototype is dangerous, because it will become harder and harder to make changes to the system and still have it behave correctly. And once the incorrectness of the system gets beyond of what the business will accept, it's very hard not to do a full rewrite, which is often very dangerous as well.
Granted, this is still what often happens ...
Dijkstra was nothing like this. In fact, he was probably one of the more practical academics (if that even makes sense to some people). He advocated top-down, logic-based methods for proving correctness that were based on incrementally transforming a high-level program specification into a final product fit for implementation. He likened it to composing music.
He also deeply studied paradigms that were firmly imperative in nature. Besides his work on semaphores for concurrency control, his deductive system of predicate transformer semantics and the Guarded Command Language built on top are some of the most comprehensive notations for imperative languages. He was also on the team that developed ALGOL 60, so it's quite likely you owe most languages you've used partially to him.
That and your conception of an academic using the analogy of the "Haskell CMS verified by Coq" is largely a straw man, though I can understand why you used it. HN is pretty crazy about these things, so it's easy to get caught up in the thought bubble thinking it's the norm.
You could stand to learn something about the Hell of fighting other people's quickly written crap just to get your job done.