Saturday, March 21, 2009

Writing about a program

I'm working on my thesis proposal.  I'm wondering what details of my theorem provers to include in a text writeup.  There are hundreds of small choices you make implementing a piece of software.  Which are important enough to explain and record, and which are just artifacts of, say a particular choice of data structure?  After reading a bunch of related papers, I think the best answer is that you should include enough information so that if you totally lost the memory of implementing the system, you could produce an "equivalent" program, i.e., one that has "roughly" the same operational behavor.  This should include the high-level optimizations.  An optimization is high-level if it operates at the level of abstraction.  For instance, if your theorem prover does term indexing, the kind of term indexing, and any non-standard tweaks, it performs should be recorded.   The actual structure should be elided.  Perhaps the best way to describe this in SML would be as "maximally abstract" signatures and functors.  Well, I obviously need to think about this more...

No comments:

Post a Comment