 When larger-scale formalizations are attempted, other challenges arise that are similar to those that software engineering tries to address.  Even fairly small programs and systems of axioms are difficult to comprehend and can be highly unpredicable, yielding unexpected consequences and unanticipated interactions.  The creation and use of larger programs and formalizations raises questions of how to enable teams of developers to produce coherent results when modules are integrated, how to maintain and test large systems, and how to use knowledge sources such as dictionaries and knowledge bases to automatically generate axioms.  