FDL notes - Scenarios of FDL Use.

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

Scenarios of FDL Use.

These scenarios are intended to prime the pump of imagination about what we think can be achieved (for a start), as well as to suggest the FDL design that supports them.

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.

1
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.

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

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

4
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.

5
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.

6a
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.

6b
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.

6c
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 P holds." The programmer asks to reexecute the proof that the invariant holds under the new assumption. The tactic is in the FDL and it is executed, revealing the need for an additional fact about streams of messages of a certain type T. This appears to be a general fact of mathematics. The programmer searches the FDL for facts about streams and finds the very fact needed to justify the proposed code modification, but the proof uses a different logic than the one the tactic is written for. The programmer asks for the fact to be translated into the tactic's logic and then runs the prover on this fact which is established automatically. The programmer is able to make a simple modification that is provably correct even though he or she does not understand formal logic.

Continued at Scenarios of FDL Use(part 2) IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

Glossary FDLnotes

1	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.

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

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

4	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.

5	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.

6a	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.

6b	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.

6c	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 P holds." The programmer asks to reexecute the proof that the invariant holds under the new assumption. The tactic is in the FDL and it is executed, revealing the need for an additional fact about streams of messages of a certain type T. This appears to be a general fact of mathematics. The programmer searches the FDL for facts about streams and finds the very fact needed to justify the proposed code modification, but the proof uses a different logic than the one the tactic is written for. The programmer asks for the fact to be translated into the tactic's logic and then runs the prover on this fact which is established automatically. The programmer is able to make a simple modification that is provably correct even though he or she does not understand formal logic.