Butler
Lampson, Jim Horning, Ralph London, Jim Mitchell, and Gerry Popek
Citation: ACM Sigplan
Notices 12, 3 (Mar. 1977), pp 11-18. Revised as Technical
Report CSL-81-12, Xerox Palo Alto
Research Center.
Links: Abstract, Acrobat. Here is an HTML version created by OCR for the benefit of search engines; it is not meant for human consumption.
Email: blampson@microsoft.com. This paper is at http://www.research.microsoft.com.
Abstract:
The programming language Euclid has been designed to facilitate the construction of verifiable system programs. By a verifiable program we mean one written in such a way that existing formal techniques for proving certain properties of programs can be readily applied; the proofs might be either manual or automatic, and we believe that similar considerations apply in both cases. By system we mean that the programs of interest are part of the basic software of the machine on which they run; such a program might be an operating system kernel, the core of a data base management system, or a compiler.
An important consequence of this goal is that Euclid is not intended to be a general-purpose programming language. Furthermore, its design does not specifically address the problems of constructing very large programs; we believe most of the programs written in Euclid will be modest in size. While there is some experience suggesting that verifiability supports other desired goals, we assume the user is willing, if necessary, to obtain verifiability by giving up some run-time efficiency, and by tolerating some inconvenience in the writing of his programs.