Functional programs are very close to semantic equations, and lend themselves readily to formal manipulation. New programs can be derived from old, or from specifications, or from a mixture of the two. There are various possible methods of derivation; the extension of existing methods and the invention of new ones to cope with more demanding problems is a primary topic of research. Calculating programs by hand can be tedious and error-prone, so another important topic of research is the design and implementation of semi-automatic calculators: the challenge is to combine rigour with convenience, and to enable productive co-operation between the human programmer and the mechanical assistant.
We have combined these lines of research in STARSHIP, a prototype system that has played host to several experiments. This interactive transformation system supports fold-unfold and simple inductive proofs in a lazy polymorphic language. It can cope with a wide range of examples, including programs involving I/O. Programmed definitions and laws introduced about them automatically persist; dependencies between them are maintained, as are all outstanding proof obligations associated with each. If any assumption turns out to be false, there is automatic roll-back of exactly those derivation steps that depended on it. A form of modularity is supported, with secure transformation across module boundaries. In addition to an inbuilt command structure, a purely functional meta-language can be used to express and execute co-operative transformation strategies for machine and programmer. There is also provision for the storage, manipulation and replay of transformational histories.