Draft Manifesto

Draft Manifesto (?) for the VS grand challenge

(This text is an attempt at the sort of text I believe we want front and center at the public home page for the challenge, i.e., a brief and engaging story that will appeal to bright undergraduates and beginning graduate students not yet decided on specialization. I'm not skilled at this sort of writing; I offer this text as provocation for someone who is. --D.N.)

The dream

Early in the history of computer programming (the 1960s) a ``software crisis'' became apparent. The need for software far surpassed the ability of programmers to produce code that could be relied on to perform its task --and to do no harm. The engineering of physical systems had by then become well organized and successful. System behavior could be predicted reliably on the basis of a tractable number of well chosen experiments or test cases. This is explained by the mathematical notion of continuity: Small variations in system inputs or component design result in small variations in behavior (except at boundary points, where testing focuses). Smoothness of variation is noticeably absent in computer systems: models of computation are based on discrete (not continuous) mathematics. Software could fail, and often did, sometimes disasterously, even after it had been carefully reviewed and validated through enormous amounts of systemmatic testing and extensive use in the field.

Thus was born the dream of program verification: System requirements could be rigorously specified using the language of mathematics, and mathematical proof could complement testing as evidence that the system's behavior satisfies the requirements. An even more spectacular dream was that a correct system could be derived from its specification, like in physical systems where parameters of a component design can be derived from requirements using calculus.

The failure

The dream captured the attention of many leading scientists and programmers in the 1960s and 70s. Initial advances were encouraging: Rules were found for reasoning about properties of computations in terms of the program text. The rules were re-cast into a deductive format based on mathematical logic. The latter field had, during the 1930s--1950s, turned reasoning into a mathematical object of study, one that appeared to be amenable to automation by computer just like the solution of differential equations.

The dream of mechanized reasoning or artificial intelligence seemed to become ever more remote during the 1960s and 1970s as initial successes opened windows onto daunting obstacles. It soon became apparent that program verification in particular would be extraordinarily difficult. Indeed, software is needed for complex tasks for which even precise specifications are elusive. The software itself is still more complex. Whether the reasoning was to be mechanized or not, proofs of program correctness were far beyond anything ever achieved or even imagined.

These lessons were learned painfully, in projects that began with grand promises but ended in failure. [for example?] One can argue about how grand those promises were. The words "proof of correctness" invite misinterpretation: what verification does is to confirm that the behaviors exhibited by a complex piece of software conform to a specification that is more easily understood than the code itself. This leaves open the possibility that the requirements are flawed or not adequately captured in the specification. Moreover, a verified program can still misbehave owing to something outside the mathematical models in which proofs are conducted. As with the notion in law, "proof" can at most mean high confidence. Still, the efficacy of mathematics in other engineering fields is undeniable.

Some concluded the dream was misguided. Many more, probably the majority of computer scientists and programmers, could appreciate that software ought to be rigorously specified and verified ---to be an engineering practice based on a science. But at the same time they saw, in the miniscule successes and big failures, clear evidence that the dream was utterly impractical. Through the 1980s and into the 1990s the complexity of software grew exponentially. The range of uses for computer systems also exploded, and the public grew accustomed to the notion that software is something subject to frequent and unpredictable errors. By this standard, ``reasonably'' reliable systems could be produced by trial and error methods. And there were real advances in the art and craft of programming.

A few researchers continued to study formal verification and some research results had modest influence, e.g., in the type systems of some popular programming languages and in a very few critical applications. But hardware capabilities grew in accord with Moore's law and software grew apace. By most standards, program verification had become a specialized research topic with little relevance to software practice.

Why now?

It hardly needs mention that computer systems are at the core of our infrastructure and pervade our personal lives. Whereas unreliability of many applications is merely annoying, there are other systems where flaws are potentially catastrophic ---e.g., pacemakers, nuclear power plants. Network connectivity, now crucial for supply and distribution chains, makes many systems attractive targets for attackers. Vulnerabilities are everywhere. The high cost of software development has led to greater distance between vendors and procurers, increasing the chance that attackers can exploit not only flaws but hidden trapdoors or Trojans.

The essential feature of software, the root of the original software crisis, is that software is discrete: tiny changes have arbitrarily large effect. This makes it certain that malicious agents can and will exploit small vulnerabilities to disasterous effect. There is reason for despair.

Yet the dream of verified software is not lost. Fully specified requirements and comprehensive proofs of correctness for large systems may be no closer to reality than ever, but in the past decade the techniques developed in pursuit of the dream have become increasingly practical. Driven by the goal of finding bugs in systems of ever greater complexity, hardware designers in 1990s found that some techniques developed as a means for proof can be highly effective at automatically finding errors. The conceptual shift from ``proving correctness'' to ``finding non-obvious bugs'' was liberating. Success led to further progress in theory and algorithms for verification. The tremendous speed and storage capacity of current hardware is also a crucial factor in achieving mostly-automated reasoning on the requisite scale.

Software is increasingly used in devices such as automobiles where safety standards, including liability in case of injury, are well established and quite strong compared with the ``no warranty'' custom for software. Prospects like automotive viruses propogated via radio navigation systems adds to the urgency of drastic improvement in security and dependability.

For these reasons and others, verification based on rigorous mathematics has become increasingly valuable and increasingly feasible. Precise specification of critical properties, and development of correct and verified software for critical systems, can now be described not as a dream but as an inevitability ---though it could take a century to become commonplace.

It will likely take a century before we colonize other planets, but the first leap to the moon was accelerated owing to the well timed launching of a grand challenge. With comparable effort we can put a proof on the moon in two decades. Seriously, we can send people to the moon in spacecraft with software systems that have been proved robust against the unavoidable failures of hardware. They will look back at the earth and know that the network infrastructure by which they send good-night messages to their families has been proved dependable and secure, even though it connects many systems running less critical software of dubious provenance and malicious software of great cunning.

The roadmap

Tony Hoare is known to every programmer for his Quicksort algorithm. He formulated the logic that bears his name, which made program verification linguistically elegant ---appealing both to logicians and to programmers who find assertions to be the best comments. He has recently provoked a debate on whether now is the time for a major international initiative, and if so what should be the roadmap. The VSR roadmap is an evolving collection of challenges and milestones being created by interested parties across the globe.

Young visionaries and seasoned ones are sought to define and prioritize the challenges, to form collaborative groups to carry out the requisite activites, and to engage in friendly competition ---sharing the resulting verified software and verification tools. Even if some milestones remain out of reach, their pursuit is sure to advance the theories, practices, and outcomes in software development. Pursuing the challenge of verified software is fun and has unprecedented intellectual depth. Among the programs to be verified are the verifiers themselves. We will make the machine think, if only about itself.