A systematic transformation method based on incrementalization and value caching, generalizes a broad family of program improvement techniques. The technique and an interactive tool, CACHET, supporting it are presented. Though highly structured and automatable, better results are obtained through interaction with an external intelligence, whose main task is to provide insight and proofs involving term equality. This process yields significant performance improvements in many representative program classes, including iterative schemes that characterize Today's hardware specifications. This is illustrated by the derivation of a hardware-efficient nonrestoring square-root algorithm. Keywords and Phrases: Formal methods, hardware verification, design derivation, formal synthesis, transformational programming, floating point operations.
