Hi Alan -- you are basically promoting the idea of driving program design via data descriptions. That is, since a program processes information, the laws of designing programs should be connected to the laws of describing information. In my terminology, information is what you find in the real world. Data is something in your language of choice that represents information. For example, in Fortran you may use 5 to represent 5cm, 5C, or $5. Over the past 30 years or so, PL designers have developed a basic language of data composition. It comes with a set of primitive operations (creation of data, extraction of values from compound data, mutation of data, recognition). The ideas (in pure form) are more or less based on the interpretation of set theory by the designer, and are thus more or less independent of the actual language (if it avoids connection between values and machine notions). One can indeed use a data description to derive programs, step by step. Our book for the TeachScheme! project (programming for high school students) is based on exactly this idea. Take a look, we distribute the book over the Web: http://www.htdp.org/ but you can also buy it :-) See the design recipes. They carry over to other FP-like languages, such as Python. I have worked with the idea for 15 years. They were developed in the functional programming community (starting with Burge's book in the early 70s). The community wasn't so much interested in correctness but in the systematic construction of programs. The layering of the idea was expounded in great detail in Abelson-and-Sussman's famous SICP. It's also on-line now. In contrast, the Hoare-Dijkstra-Gries school of thought was interested in correct algorithms. When you work in their (wp or sp) logic, you write the program first -- in an ad hoc manner, w/o any underlying laws -- in an extremely low-level quasi-functional language of logic. Then you derive the program again, by hand. One could some of that via machine. In any case, their work never truly scaled beyond procedure bodies, because they couldn't get anythig but :=, begin, while, and if to work completely. [Okay, I know there is more, but don't bother me with details. That's the gist of it.] -- Matthias