Formal methods imply a distinctive view of software development. According to this view, the software engineer's task is to produce several models or descriptions of a system for an abstract machine, with accompanying proofs that models at lower levels of abstraction correctly implement higher-level models. The job of the hardware engineer, language designer, and compiler writer is to provide a realization suitable for executing the applications developer's abstract model, but it is not the application programmer's job to twist his logic to fit inadequate physical automata. Only this idealized design process can ensure high levels of quality, not testing. Testing can demonstrate the presence of faults, not their absence.
