"The practice of supplying proofs for nontrivial programs will not become widespread until considerably more powerful proof techniques become available, and eve

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