Clearer distinction between recommendations to library authors vs. parameters for reasoning purposes in the formalism.

[zenhack]

Based on conversation in #23: right now the configuration C is serving double duty as abstracing out some parameters for the purposes of the formal description, and also as something that might be literally exposed by a library. There's some tension here, since some things are convenient to talk about as parameters for the formalism's purpose, but should not actually be exposed to library users for one reason or another.

We should properly separate these concerns, talking about recommendations for library interfaces in a separate section.