[lliamander]

This is similar to an intuition I've had about what it means to program "algorithmically". We often draw a distinction between "algorithms" and "business logic", but fundamentally they are the same thing. They are both plans of the steps necessary to accomplish a goal. The only difference, in my mind, is the style in which the program is written. To program "algorithmically" means to take steps to make undesirable program states impossible to represent.

- In the case of search or sort algorithms, where the primary concern is the speed of computation, undesirable states would be performing unnecessary or duplicate computations.

- In the case of encryption algorithms, undesirable states would be those that leak encrypted data.

- In the case of an order shipping and fulfillment system, an undesirable state would be marking an order as fulfilled when not all of the items have been delivered.

The more care that is taken to prevent undesirable states, the more the program takes on an algorithmic style. And the only way you can be sure that those undesirable states are impossible is to think in terms of proofs and invariants.