The best way to document a program is to prove its correctness. Short of that, it is usually no fun to deal with other peoples (or your own old ones) programs a

The best way to document a program is to prove its correctness. Short of that, it is usually no fun to deal with other peoples (or your own old ones) programs anyway. As for presenting things in the right order: This order would largely be imposed by a correctness proof. As there could be different proofs, there could be different orders. Obviously, not all programs can be proven correct (but I think a very large part of all programs could be). Also, finding the right order is not as difficult as finding the right level of abstraction. Once you have the right level of abstraction for presenting something, everything else flows from that.