Hoare outlines the idea that computer programs can be formally proven to be correct in the same way as other fields of mathematics by defining axioms as a logical foundation and applying deductive reasoning1. The paper lists a small set of axioms for arithmetic operations on finite integers2 and defines a simple programming language with axioms on assignment, consequence3, and iteration. With these in place, we can deduce provably correct statements about the conditions of variables at the end (or at intermediate points) of program execution. Often more than half of a program’s development time comes from testing and debugging, which emphasizes the importance of proving correctness.
I’ve written plenty of incorrect code in my day, so the promise of provenly correct code is enticing. I’m curious as to how much time would be needed to formally prove a program correct compared to traditional testing methods. My guess would be that the complexity of proofs grows more quickly than that of programs, so they soon become intractable for programmers to reason about mentally. Taking an approach of partitioning a program into smaller logical sections (much like Hoare’s axiom of consequence) and proving each of these would be much easier to manage.
I also wonder how established axioms could inform the design of algorithms so that they are more naturally provable, rather than contorting the axioms to fit with whatever code you’ve already written.