Goals of Unifying Theories

Unifying theories is one of the major goals for every branch of science, and it is considered worthy of pursuit as an intellectual achievement for its own sake. A successful unification demonstrates that a number of existing experimentally supported theories are special cases derivable from some more general theory; and the general theory often turns out to be the simplest member of the family. Study of such a unifying theory often suggests new special theories that can independently verified and applied. Confidence in the validity of all the theories involved is greatly increased. Quantum theory is a superb example of such a grand unification.

In the study of the theory of programming and the semantics of programming languages, there are already a great many elegant and useful theories. Some of these have been incorporated into tools supporting the various phases of a software project -- design, development, testing, verification and evolution of computer systems, both in hardware and in software. Many successful tools have exploited particular characteristics of their intended application area, or they are restricted to a particular design pattern or paradigm of system implementation. Many tools are rightly targeted at only one phase of the software project. For this reason, the most successful tools are often used in an ad hoc combination with other tools, some of which have a less secure theoretical foundation.

Unifying the theories that underlie wider ranges of software tools will give a theoretical foundation for the combined use of the tools, each of which can be more confidently specialised to its particular function. It will ensure that there are no gaps in the chain of evidence that validates the software product. It will reduce the conceptual mismatches that unnecessarily complicate the learning of new tools. And it will be a worthwhile intellectual achievement for its own sake. Research into unifying theories can proceed simultaneously from the bottom up and from the top down. Bottom-up research can start with a selection of existing specialised tools that have proved their value in application; and it can explore the unifying theories that would support their use in combination. Where tools are in direct competition, a unifying theory can help to resolve the issues in a sound scientific spirit. In all cases, the possibility of removing unnecessary complexity and inconsistencies will be revealed.

Top-down research is more idealistic, less tied to existing languages, tools, applications, and processes. The goal is to provide a general theory of correctness of programs, including their necessary links to specifications. The challenge is to combine, yet keep separate, the main features of modern programming -- concurrency, non-determinism, object orientation, transactions, etc. Its methods are those of programming language semantics. A successful unification will link the presentation of semantics in the operational, algebraic and denotational styles. The operational style is essential for program testing and model checking; the denotational style is appropriate for the design of specification languages and the proof tools that support reasoning about correctness; and the algebraic style provides a useful bridge between the two. The unification is essential to validate the reliable use of model checking in combination with proof, and to formalise and prove correctness of program verifiers and programming language compilers. And the intellectual achievement would serve as a foundation for a major strand in the study of Computer Science.