ABSTRACT
While computing machines execute instructions uniformly giving the same minute attention to each of their thousand and one line codes, programmers need procedures and other higher-level constructs because they must understand their programs. In its simplest form, a procedure call is just text substitution. The assertional proof method, tied to the single-level analysis of changing states, is closely related to the machine language level and not, so it seems, to the higher-level events generated by the procedures. Finding an appropriate degree of formality (or informality) is very important for those who appreciate the usage of proof to clarify ideas and concepts. States and histories specify internal semantics, while events and system executions are for external semantics. This distinction has lead to a strict notational policy of separating assignments (which are internal operations) from external operations such as reading and writing on registers.
