Sixty-five years after the birth of ENIAC, software controls airplanes, pacemakers and missile systems�and it's buggy. Nonetheless, provably correct software has come a long way, and a variety of emerging software testing frameworks and methodologies are poised to further advance the cause.
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.
