Specifying, Programming and Verifying with Equational Logic

1 Introduction Programming is difficult, as shown by the fact that debugging a program usually takes more time than creating it; moreover, the difficulty of debugging increases non-linearly with program size. One reason for such phenomena is the astonishing complexity and subtlety of the semantics of most widely used programming languages, due mainly to the desire for high efficiency on conventional processors. But rapid increases in the power and flexibility of hardware, and in the need for greater reliability and security in applications, suggest that it may be valuable to consider alternative approaches, based on higher level languages with much simpler semantics, despite the undoubted inertia of tradition, and the difficulty of learning new languages and new paradigms. This paper focuses on the OBJ family of languages, which have semantics based on various extensions of (first order) equational logic. The OBJ languages are logical programming languages, in which programs are theories, and computation is deduction, which makes it possible to do specification, programming and verification in a unified framework. This paper is mainly intended to introduce and motivate the material that it covers, rather than to provide a thorough mathematical exposition. Consequently, there are many references and several examples, but all proofs and many technical details are omitted