History for Draft Manifesto

changed:
-This is explained by the mathematical notion of continuity: small variations in
-system inputs or component design result in small variations in behavior.
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).  

changed:
- Thus was born the dream of program verification: System requirements specified
-rigorously using the language of mathematics, and mathematical proof that the
-system's behavior satisfies the requirements.
-Some went even further, dreaming that a correct system could be derived from its
-specification just as in physical systems where a component design can be derived
-from requirements using calculus. 
 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. 

changed:
-The software itself is still more complex.  Whether the reasoning was to be
-mechanized or not, such proofs were far beyond anything ever achieved or even imagined.
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.

changed:
-but ended in failure.
but ended in failure.  [for example?]

changed:
-The words ``proof of correctness'' invites 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.
-
- 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 that the dream was utterly impractical.
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.

changed:
-The range of uses for computer systems also exploded, and the public grew
-accustomed to the notion that software is something subject to frequent
The range of uses for computer systems also exploded, and the public grew accustomed to the notion that software is something subject to frequent

changed:
-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.
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.

changed:
-The high cost of software development has led to greater distance between
-vendors and procurers, increasing the chance that attackers can exploit not only
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

changed:
-Seriously, we can send people to the moon in craft whose software systems 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.
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.

changed:
- Young visionaries and seasoned ones are sought to define and prioritize the
-challenges, to form collaborative groups to carry out the requisite activites
-and share the results.  Even if some milestones remain out of reach, their
 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