I find myself sympathetic to [many of the things that Dijkstra says](https://twitter.com/dijkstraquotes), and really wanting to believe them.  Yet, practical experience has shown me that they're a poor match for - and I hate saying this phrase so much - the "real world" of the "software engineering" "industry".

----
I mean, the man deserves a lot of credit.  At the very least, he [saved us from the Combine](https://twitter.com/bodil/status/372739264972197888/photo/1).

----
However, as evidenced by [many](http://www.cs.utexas.edu/users/EWD/transcriptions/EWD06xx/EWD638.html) of [his](http://www.cs.utexas.edu/users/EWD/transcriptions/EWD05xx/EWD524.html) [writings](http://www.cs.utexas.edu/users/EWD/transcriptions/EWD05xx/EWD566.html), Dijkstra is a big fan of formal proofs of correctness.

----
I would also like to be a fan of formal correctness proofs.

----
The problem is, I can't convince myself that they make economic sense.

----
Formal correctness proofs – much like another of Dijkstra's bugaboos, static type systems – are a substantial amount of effort to use.  Formal correctness proofs are *so* difficult to use that I'm not aware of any research project to validate their effectiveness, but [static type systems are the closest thing we have in the field of software industry to provably worthless](http://neverworkintheory.org/2012/10/25/an-experiment-about-static-and-dynamic-type-systems.html).

(To be fair, *my* favorite bugaboo, test-driven development, also has [relatively weak empirical support for its benefits](http://neverworkintheory.org/2011/08/31/comparing-the-defect-reduction-benefits-of-code-inspection-and-test-driven-development.html).  But of course in the case of the thing that I _like_, the study was flawed and in the case of the thing that I _don't_ like, one study is definitive.)