In this paper we describe progress towards a theory of program development by systematic refinement beginning with a clean, functional program thought of as a specification. Transformations include reuse of storage, and re-representation of abstract data. The transformation rules are based on a theory of constrained equivalence for functional languages with imperative features (i.e. Lisp/Scheme/ML). Constrained equivalence is a relation between sets of constraints (on computation contexts) and pairs of expressions. The interpretation is that in all contexts satisfying the constraints, evaluation of the expressions is either undefined or produces the same results and has the same effect on memory (modulo garbage). Constrained equivalence naturally allows reasoning by cases and permits use of a variety of induction principles. An inference system for constrained equivalence that is complete for expressions not involving recursively defined functions has been developed by the authors. One difficulty with constrained equivalence is that it is not a congruence. One cannot, in general, place expressions equivalent under some non-empty set of constraints into an arbitrary program context and preserve equivalence. For this and other reasons, we have developed a formal system for propagating constraints into program contexts. In this system, it is possible to place expressions equivalent under some non-empty set of constraints into a program context and preserve equivalence provided that the constraints propagate into that context. Constrained equivalence and constraint propagation provide a basis for systematic development of program transformation rules. In this paper we present three main rules: subgoal induction, recursion induction, and the peephole rule. Use of these rules is illustrated by the transformation of a simple, but non-trivial, rewriting program, known as the Boyer Benchmark.