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

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 ? 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.