Toward The Rigorous Use Of Diagrams In Reasoning About Hardware

The logician’s conventional notion of proof has grown increasingly anachronistic through the twentieth century as computing capabilities have advanced. classical proof theory provides a partial model of actual mathematical reasoning. when we move away from mathematics toward reasoning in engineering and computation, its limitations are even more pronounced. the standard idea of a formal system seems frozen in the information technology of frege’s time; it is decidedly quaint in the presence of today’s desk-top computer. contrary to formalists’ dogma, experience suggests that pictures, diagrams, charts, and graphs are important tools in human reasoning, not mere illustrations as traditional logic would have us believe. nor is the computer merely an optimized turing machine. the computer’s graphical capabilities have advanced to the point that diagrams can be manipulated in sophisticated ways, and it is time to exploit this capability in the analysis of reasoning, and in the design of new reasoning aids. in this chapter, we propose a new understanding of the role of various sorts of diagrams in the specification and design of computational hardware. this proposal stems from a larger project, initiated by barwise and etchemendy [1991a], the goals of which are to develop a mathematical basis from which to understand the substantive logical relationships between diagrams and sentences, and to develop a new generation of automated reasoning tools from that basis. microelectronic cad systems are among the supreme examples of visualized reasoning environments. their tools are highly oriented toward diagrams, are quite sophisticated, and are comparatively well integrated. these systems also integrate logical and physical design, providing a strong coherence between specification and implementation views. formalized reasoning meshes poorly with these working frameworks. although it provides needed rigor for today’s highly complex design challenges, its preoccupation with formulas at the expense of diagrams is simply too cumbersome. we should attempt to draw lessons from these advanced design environments, making the reasoning rigorous without subverting their character. this chapter is built around a simple design example, a synchronizing circuit. our purposes are, first, to illustrate heterogeneous use of pictoral “formalisms” in design, and second, to expose basic questions for the logical analysis that follows. we will develop a mathematical basis in which the example can be analyzed. these are admittedly modest beginnings, but we hope that they start to put to rest the idea that only formulas can be used in formal reasoning about hardware.