What Kinds of Facts About Problems, Procedures, data Spaces, Programs, And Computers Would We Like to Derive?

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:

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