Notes on the design of Euclid

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.