The role of logic in software enterprise (panel paper)
Władysław M. Turski · International Conference on Software Engineering · 1985
The history of advances in programming - the little that there is of it - is the history of successful formalisation: by inventing and studying formalism, by extracting rigorous procedures, we progressed from programming in machine code to programming in high level languages (HLLs). Note that before HLLs were sufficiently formalised compilers used to be unreliable and expensive to use, programs could not be ported between machines, and the very use of HLLs was more or less restricted to academia. Observe also that if today a piece of software is still difficult to port it is almost invariably due to a deviation from strict formality.For many application domains HLLs provide an acceptable linguistic level for program (and system) specification. One does not hear horror stories about computer applications in such domains (physics, astronomy). The expert views of such domains, their descriptive theories, can be easily expressed on the linguistic level of HLL, thus becoming prescriptive theories (specifications) for computer software. If it is desired to use computers reliably in domains where this is not the case, then we must try to narrow the gap between the linguistic level on which domain-descriptive theories are formulated and the linguistic level on which programs are prescribed (specified).The programs, as ultimately run, are always formal objects. A rigorous, calculably verifiable relationship may be defined only between formal systems (scientific theories of nature are not calculably verified; they are tested by experiments!). Therefore, if we want the programs to reliably satisfy their specifications, the latter must be formal objects too. Or, put it differently: from a natural domain to a formal system there cannot lead an unbroken chain consisting of calculably verified steps only. There must be an interface at which the informality of a natural domain (or its description) comes into contact with the formality of a computer program (or its specification). Such a watershed interface can be avoided only if the application domain is itself formal (e.g. mathematical).The problem statement at the watershed interface is crucial for the eventual success of any computer application: if it is formal, we stand a chance of developing and implementing a provably correct solution, but we cannot prove its validity in application domain. The informality of problem statement does not help a bit: it is still impossible to prove the validity and we cannot guarantee correctness of eventually implemented software. Taking the lesser of two evils, we choose a formal problem statement and call it the specification.Basically, there are two policies with respect to selection of the watershed linguistic level. They can be roughly characterised by the size and structure of the extra logic component (EC) of that level. We may opt for as big an EC as we can handle in our formal system, or for an EC not larger than necessary to validate the problem statement in application domain. The large EC policy corresponds to axiomatisation of individual elementary observations (as exemplified by Horn clause and other data-based specifications); the small EC, to axiomatisation of 'laws' abstracted from and validated by elementary observations within the application domain (as illustrated by physical sciences). Notice, however, that the choice of EC is almost entirely domain-dependent, determined by the availability (or otherwise) of well-tested developed theories for each individual domain.Invention, formulation and validation of domain-descriptive theories is, of course, the main activity of scientifically-minded experts. Nothing in a software engineer's education entitles him to claim the necessary knowledge and experience. Similarly, no results of computing science entitle computing scientists to claim that theory-forming research in application domains can be reduced to collecting elementary observations. And logic does not recognise the notion of intra-domain validity.Logic - a calculus of formal systems - plays an important role in software development from specification to implementation. It also can play a minor role in validation of specifications, insofar as the validation may be seen to include derivation of consequences. That logic plays no discernible role in descriptive theory formation - an act always serendipitous and contingent on invention - should not worry us too much, as long as we do not wish to claim the possession of the philosopher's stone.