Hacker News Reader

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.

Shipping a product with sqlite doesn't contradict with having well structured code.

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

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

You could stand to learn something about the Hell of fighting other people's quickly written crap just to get your job done.

It is this approach that leads to the "Full Employment Act of Security Professionals" everywhere.

Part of being a good software engineer is knowing when to do the "wrong" thing (implement something poorly to ship fast). But you must be aware of the trade offs. For early stage companies/products that are struggling for a market it often makes sense to hack things, but at a company that has a large and growing customer base, it rarely does.

There is also tons of examples of companies going bankrupt because they did not thought they would be consequences by shipping a half-baked product. It's just that sometimes you need to prioritize shipping and sometimes you really need a good product quality, it depends on a lot of factors and the business you are in.

Dijkstra doesn't do any work, he's been dead since 2002.

Well sure, but you can find your beliefs in ivory towers too. Also, argument is central to academia or my impression of it anyway.

May you be cursed to spend the rest of your days writing PHP.