Gerry Popek, Butler
Lampson, Jim Horning, Ralph London, and Jim Mitchell
Citation: ACM Sigplan
Notices 12, 3 (Mar. 1977), pp 11-18.
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:
Euclid is a language for writing system programs that are to be verified. We believe that verification and reliability are closely related, because if it is hard to reason about programs using a language feature, it will be difficult to write programs that use it properly. This paper discusses a number of issues in the design of Euclid, including such topics as the scope of names, aliasing, modules, type-checking, and the confinement of machine dependencies; it gives some of the reasons for our expectation that programming in Euclid will be more reliable (and will produce more reliable programs) than programming in Pascal, on which Euclid is based.