Semantic Foundations for Interactive Programs

When we first explain how computer programs work to beginners, we tend to explain them as a way of telling a computer how to implement an input-output relation: matrix libraries take a system of linear equations and compute a solution; compilers take a source text as input, and produces an object file as output; and web browsers read an HTML file as input, and then renders it to a screen as output. However, the programs we actually use tend to be interactive. Instead of solving a system of equations once, we might put it into a spreadsheet and incrementally modify the parameters to explore the solution space. Instead of giving a program once to a compiler, we develop within an IDE, with our work flow interleaving the process of writing code and finding and repairing errors in the program. A web browser does not merely display an HTML document, but can programmatically update the page in response to user and server events.

However, implementing interactive programs is generally much more complicated than implementing one-shot input-output behaviour. Programmers do not get the input to their program all at once, but instead they get it piece-by-piece incrementally. Furthermore, the output also has to be produced incrementally, so that the user of a piece of software can observe and react to the output produced so far. As a result, ensuring that the program keeps track of the user inputs and maintains a consistent view of what the user wants is quite difficult. Furthermore, the interactive behaviour of the program also makes it is harder to say what is and is not correct behaviour for the program, so even telling if a program is correct or incorrect can become very difficult.

The purpose of this project is to develop new programming languages that make writing interactive programs easier, in two ways. First, we will develop mathematical techniques to make it easier to formally state what a program should do, and to check that programs are satisfy this specification, and second, we seek to develop implementation techniques that ensure that interactive programs can run efficiently and respond in a timely fashion to user inputs.

Interactive programs pervade software development, and nearly every
program that every person uses is an interactive program. The
proposed research studies the foundations of reactive programming, and
so is likely to be of interest to anyone interested in
understanding, writing, or using interactive programs.

It is useful to imagine the beneficiaries of the proposed research as
falling into three tiers.

The first tier are other researchers in the areas of programming
languages and semantics. Interactive programming supplies many novel
challenges in program verification and type theory, and having a
rigorous mathematical language for talking about time-dependent
properties is very likely to be useful for modelling and proving the
properties of many kinds of software systems beyond interactive
programs.

The second tier are practitioners interested in building reactive
systems. There is already widespread commercial interest in reactive
programming (for example, see the Reactive Manifesto at
http://www.reactivemanifesto.org), and there are numerous popular
libraries and implementations (such as RxJava, React, Meteor, and
WPF) which support significant amounts of reactive-style programming.

However, each such library implements a different subset of
functionality, with different choices made depending on the facilities
of the underlying language and the performance costs of the chosen
implementation strategies. As a result, it is very difficult to
compare different reactive programming libraries. It is also quite
difficult to understand which facilities are essential, and which
merely add complications without a corresponding benefit in terms
of expressive power. Overall, it is quite difficult to understand
how programmers can build their own abstractions on top of the
supplied primitives, or even what primitives should (or should not)
be supplied.

The proposed research takes a foundational approach to this question,
basing the high-level design on fundamental logical concepts, and
seeking to design low-level primitives which are clean and orthogonal
enough to permit formal correctness proofs. This is very likely to
lead to powerful conceptual guidance for working programmers, and the
"Pathways to Impact" document highlights the priority we place on
communicating these ideas to them.

The final tier are users of interactive programs. Everyone who uses a
computer does so through an interactive interface, and so everyone has
an interest in this interface working well. Furthermore, much private,
important, or otherwise security-critical data is communicated to
users via interactive programs, and it is important to ensure not just
that the right data is communicated, but that is made available only
at the right times.

For example, we might want a guarantee that a banking application
never reveals any financial data before it receives a correct
password. Note the use of the word ``before'': we definitely want the
program to reveal private data, but only after the correct password
has been supplied. It is precisely properties like this that the
proposed research studies, and so I believe that this work will help
make software more secure, reliable and trustworthy.