Limits of Heroism

There has been much nice work lately on proving that complex software is written correctly, including components like operating systems, compilers. But it’s hard to see how to scale these heroic efforts to the vast amount of software that is being written every day. It’s simply too hard to build software that is correct and secure. Much of the problem arises because of the low level of abstraction at which software is written. We’re fighting a war on which (not to be dramatic!) the future of civilization may depend, and right now we’re only winning scattered battles. The problem is that we’re fighting this war on the wrong terrain—such as the terrain of C and C++ code, where even the most basic security and correctness guarantees are absent. We need new language design research that moves the field of engagement to more favorable terrain, because your strategy for winning a war can’t rely on the existence of heroes.