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