Lambda the Ultimate

Mindless Coding, uses Coq to emit Ocaml:

Fully-specified dependently typed structures (avltree and rbtree) and their functions (find, insert, delmin and delete) not only produce fully verified results - they also reduce the task of function implementation to a stepwise refinement of intermediate steps (proof subgoals) that are constrained to the point where the programmer (prover) is freed from consideration of the overall algorithm involved during each step. In many cases, the steps are fully automatable. In others, the information provided by the subgoal's context, along with a "rough idea" of what the algorithm being implemented should do, is usually sufficient for the programmer to make progress to the next subgoal.

Perhaps the best illustration of this "mindless" point is the implementation of the complex rebalancing functions for Red-Black trees, which are widely viewed as difficult to do correctly. These were implemented using this "mindless-coding" technique without relying on any outside explanatory material or implementations.

'Mindless' if you are smart enough to be able to do incremental steps in proof-making :-)