Primarily. we would like to be able to prove that given procedures solve given problems. However, proving this may involve proving a whole host of other kinds of statement such as:

- Two procedures are equivalent, i.e. compute the same function.
- A number of computable functions satisfy a certain relationship, such as an algebraic identity or a formula of the functional calculus.
- A certain procedure terminates for certain initial data, or for all initial data.
- A certain translation procedure correctly translates procedures between one programming language and another.
- One procedure is more efficient than another equivalent procedure in the sense of taking fewer steps or requiring less memory.
- A certain transformation of programs preserves the function expressed but increases the efficiency.
- A certain class of problems is unsolvable by any procedure, or requires procedures of a certain type for its solution.

Tue May 14 13:32:03 PDT 1996