These scenarios were generated by a combination of recalling some that have been discussed among our group before, as well as reading through these notes and producing scenarios they rather directly suggest; they seem obvious to us because of prior discussions, a certain familiarity with the use of the FDL concepts, and our experiences in the actual production and manipulation of formal and informal content.
A reader wants to find what material there is in a library concerning a subject or a particular idea. They start by looking for keywords, which builds a collection of informal documents that mention the keys, and a collection of concise titles and paraphrases of formal objects that mention the keys. The reader then conducts further searches which can be based upon the formal structure of objects now discovered to be relevant. 

A student wants to read supplemental material because the course text is unclear or obviously wrong on some point. 

A teacher wants to ascertain the suitability of some material in the FDL as class material. 

A teacher wants to reorganize some material for accessibility by a class, leaving the formal material alone. This person is contributing a "reading", and it can be made easily available to others. 

A teacher wants to modify or add some formal material to an extant body, either to fill in pedagogical lacunae or to give variants of formal objects more appropriate for the students; the new formal material is as trustworthy as the old assuming it uses the same logical basis. 

A programmer wants a precise explanation of a standard (perhaps common, perhaps obscure) algorithm to know why it works in order to implement a variant of it. To her delight, she finds several reference algorithms using different representations of the data. There is one part of one of the more familiar algorithms that has always seemed unnecessarily complex; by digging into the formal proof of its correctness she finally sees what she was missing. 

A user (or manager or programmer) learns that there are documents in the FDL about the MediaNet distributed computing system for video. Examination reveals pertinent formal definitions and proofs about the schedule checker for quality of service, constituting conclusive documentation grounded in the formal material. A particularly helpful experience involves understanding a "stream transformer". Because the transformer function was defined constructively it can be run on examples by an interpreter invoked by the FDL, ie, there is a "dynamic model" of the stream transformer available from the FDL based on the constructive content. 

A programmer must modify a protocol in the event processing protocol stack of a system, due to changes in the upstream processes. The formal documentation of this protocol in the FDL system/theory entry for the stack states assumptions about the input stream and invariants of the protocol. It is not clear to the programmer that the new message stream will satisfy the input assumptions. Further investigation of the upstream process, also in the FDL, reveals that the assumption is violated in a way that can be described by simple additional clause such as "or condition 
Continued at