February 14, 2013, 7:16 AM — We can get CPUs that are consistent and reliable, and we can get compilers that work on top of them that are provably correct. Pascal creator Nicholas Wirth described how to write a correct compiler in his book, Compiler Construction, back in 1996. It should be a simple step from there to create "functionally correct" programs that can, for any input, produce the correct output.
The only problem is that no one seems to be able to actually do it.
From Complete Testing to Proofs
Dutch computer scientist Edsger W. Dijkstra is renowned for his contributions to programming languages and for creating the phrase "Go to Considered Harmful."
Within testing circles, he is known for his proof that testing addition for two 32-bit integers a microsecond at a time, would take longer than the known history of the universe. (The problem isn't the 32 bits but that two variables together create 64 bits of combinations.) This leads to Dijktra's famous quotation: "Testing can show the presence of errors, but not their absence."
Most programs are more complex than adding two numbers together. This leads some academics and practitioners to abandon testing and to pursue "proof of correctness" instead. These proofs can demonstrate that a requirements document, probably expressed in symbols, is correctly implemented in code.
Wirth argues that proofs of correctness should be included in programming courses in undergraduate computer science, while C.A.R. Hoare proposes the Floyd-Hoare notation. Sidney L. Hantler and James C. Kind, meanwhile, provide an excellent introduction to proving the correctness of programs, making it clear that the size of the proof will grow much faster than the code itself.
In other words, where the code for a 10-line procedure could be proven in an academic exercise, it's just not feasible for a real, industry computer program. This problem of exploding complexity in code is not new. The NATO Software Engineering Conference identified is as the "software crisis" back in 1968.
Where "proof of correctness" may not be feasible, there have been attempts to move in that direction, to provide more rigor and correctness around a program before it gets to testing. A few of the more popular ways to address this include the transformational specification, model-based testing and Fred Brooks' "Bronze Bullets." Each is discussed below.
Transformational Specification: Impractical for Software Development