Refinement style programming

This style of programming provides a way to build the program and its justification hand-in-hand. It is possible to gradually refine these two objects, filling only as much detail as necessary for clarity. So for example, proof detail can be omitted for programming steps that are obvious. The extreme case of ``unbridled'' programming arises when we omit all proof steps except those that come automatically as part of the programming, e.g. certain ``type checking steps'' and the over all logical structure of the proof.