"The practice of supplying proofs for nontrivial programs will not become widespread until considerably more powerful proof techniques become available, and even then will not be easy. But the practical advantages of program proving will eventually outweigh the difficulties, in view of the increasing costs of programming error."

The Hoare paper actually linked is hopelessly outdated, despite being an interesting historical artifact.

I might call it "sadly" outdated... not that I'm a fan of provably-correct programming (I've never done it, I just fix systems and networking software), but the seemingly modern comfort with buggyness and sloppy implementation... funny or sad, who knows