Formal Methods

I find myself sympathetic to many of the things that Dijkstra says, 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.

However, as evidenced by many of his writings, 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.

(To be fair, my favorite bugaboo, test-driven development, also has relatively weak empirical support for its benefits. 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.)