Some theorems we should prove

Mathematical techniques can be used to produce precise, provably complete documentation for computer systems. However, such documents are highly detailed; oversights and other errors arc quite common. To detect the “early” errors in a document, one must attempt to prove certain simple theorems. This paper gives some examples of such theorems.