Since Elephant 2000 programs will be sugared versions of logical sentences, their properties will be logical consequences of the sentences expressing the program, the axioms of Elephant 2000 and a theory of the data domains (if any) of the program. In this Elephant resembles Algol 48 and Algol 50 described in a later section.
(more to come)