Unifying theories of programming
A theory of programming is intended to support the practice of programming by relating each program to the specification of what it is intended to achieve. A unifying theory is one that is applicable to a general paradigm of computing, supporting the classification of many programming language as correct instances of the paradigm.
A diversity of presentation is seen in a theory of programming, which has to explain the meaning of the notations of a programming language. An investigation from the top-down starts with an attempt to understand the system as a whole. It is always relevant to ask first what is its purpose? What are the requirements of its users? The next step is to identify the major components of the system, and ask how they are put together? How do they interact with each other? What are the protocols governing their collaboration?
As a result, a top-down theory of programming starts from the denotational definitions and continues by formalization and proof of theorems that express the properties of all programs written in the language. The goal is to assemble a collection of laws that will be useful in the top-down design of programs from their specifications, and ensure that the resulting code is correct by construction. Investigation of a complex system from the bottom- up starts with an attempt to discover a minimum collection of primitive components from which it has been made. These are assembled into large components by primitive combinators. The notations chosen to denote these primitives and combinators constitute the syntax of a simple programming language. Their operational meaning is defined by enumerating the kind of primitive steps that will be taken by the machine in executing any program that is presented to it. The theory may be further developed by investigation of properties of programs that are preserved by all possible execution steps. The resulting classification of programs is presented as a set of axioms that can be used in proofs that a program enjoys the relevant properties. The properties are often decidable, and the axioms can be used as a type system for the programming language, with conformity checkable by a compiler.
The benefits of a top-down presentation of a theory are entirely complementary to those of a bottom-up presentation. The former is directly applicable to discussion and reasoning about the design of a program before it has been written, and the latter to the testing, debugging, and modification of code that has been written. The advantages of both approaches can be confidently combined, if the overlap of laws provided by both of them is sufficiently broad. The laws are specification of the common interface where two approaches meet in the middle.
- J. He. Let's unify theories of programming. Lecture slides from EWSCS 2014.
- Videos from the lectures.
- C. A. R. Hoare, J. He. Unifying Theories of Programming, Prentice Hall Int. Series in Comput. Sci. Prentice Hall, 1998.
May 21, 2016 23:39 EET
local organizers, ewscs14(at)cs.ioc.ee
EWSCS'14 page: http://cs.ioc.ee/ewscs/2014/