Theorem proving and software engineering

The author discusses the potential role of computer support for theorem proving in software engineering. There are three major approaches into which most formal methods can be divided. That which fits the normal development route most closely is to fix a specification notation but to record design by bringing in features of the implementation language. Such design steps give rise to `proof obligations´ which are sentences in a logical language; their discharge justifies the design. An alternative approach is to make the initial description a very clear, but probably hopelessly inefficient algorithm. This is transformed in a series of steps to a workable program. Each transformation step is an instance of one of a number of general rules. A few of these are universal; most have applicability conditions which again result in proof obligations. A third, newer, approach extracts algorithms from constructive proofs of the existence of a result satisfying a specification. Putting aside the difference between approaches, it is clear that each needs proofs. Software engineers of the future will use these tools (on critical applications) in the same way that engineers in other disciplines use mathematics thought too complex by the first `pragmatic´ practitioners