The Alma Project, or How First-Order Logic Can Help Us in Imperative Programming - Correct System Design: Recent Insights and Advances - page 85

\market" will eventually pick up the best product. Such a reasoning would be
correct if the market forces in computing were driven by the desire to improve
the quality of programming. But from an economic point of view such aspects
as compatibility and universal availability are far more important than quality.
Having this in mind we would like to put the above factors in a proper per-
spective and instead concentrate on the criteria that have been used in academia
and which appeal directly to one of the primary purposes for which a program-
ming language is created, namely, to support an implementation of the algo-
rithms. In what follows we concentrate on the subject of \general purpose"
programming languages, so the ones that are supposed to be used for developing
software, and for teaching programming.
Ever since Algol-60 it became clear that such programming languages should
be \high-level" in that they should have a suciently rich repertoire of control
structures. Ever since C and Pascal it became clear that such programming
languages should also have a suciently rich repertoire of data structures.
But even these seemingly obvious opinions are not universally accepted as
can be witnessed by the continuing debate between the followers of imperative
programming and of declarative programming. In fact, in logic programming
languages, such as Prolog, a support for just one data type, the lists, is provided
and the essence of declarative programming as embodied in logic and functional
programming lies in not using assignment.
Another two criteria often advanced in the academia are that the program-
ming language should have a \simple" semantics and that the programs should
be \easy" to write, read and verify. What is \simple" and what is \easy" is in
the eyes of the beholder, but both criteria can be used to compare simplicity of
various programming constructs and can be used for example to argue against
the goto statement or pointers.
In this paper we argue that these last two criteria can be realized by basing
a programming language on rst-order logic. The point is that rst-order logic
is a simple and elegant formalism with a clear semantics. From all introduced
formalisms (apart from the propositional logic that is too simplistic for program-
ming purposes) it is the one that we understand best, both in terms of its syntax
and its semantics. Consequently, its use should facilitate program development,
verication and understanding.
One could argue that logic programming has realized this approach to com-
puting as it is based on Horn clauses that are special types of rst-order formu-
las. However, in logic programming in its original setting computing (implicitly)
takes place over the domain of terms. This domain is not sucient for program-
ming purposes. Therefore in Prolog, the most widely used logic programming
language, programs are augmented with some support for arithmetic. This leads
to a framework in which the logical basis is partly lost due to the possibility
of errors. For instance, Prolog's assignment statement Xist yields a run-time
error if t is not a ground arithmetic expression.
This and other deciencies of Prolog led to the rise of constraint logic pro-
gramming languages that overcome some of Prolog's shortcomings. These pro-