In the late 60s, Bob Floyd and Tony Hoare discovered the concept of program correctness. Some people initially working on program correctness thought that, in the future, everyone would prove that their programs were correct. Programming errors would then disappear. They soon learned how naive that hope was. Floyd and Hoare showed that they could, in principle, do this. But in practice, it turned out to be very hard. Today, everyone knows that verification is economically feasible only in a small number of applications - mainly, for fairly small programs that perform life-critical functions.