The 'literate' programming model is extended to include a concept of mechanical transformation. A prototype tool, FLP (Formal Literate Programming tool), has been developed which uses this extended 'iterate' programming model in both a formal program proof setting, and within a formal (refinement) program development setting. In both settings, FLP provides history, access to tools, and an easy- to-use interface. FLP is a system with

•a tree structured revision control system allowing easy access to an entire software development history,

•a unifying semi-formal model encompassing both program proof and refinement, and

•a single simple mechanism for managing both formal transformations on programs (proofs, tests, refinements) and informal transformations (explanations).

In this paper, we outline the underlying semiformal model for this extended 'literate' programming tool, briefly show the system architecture, and demonstrate the tool's use during a sample program development.