The Choose-Your-Own-Adventure Calculus

Abstract

In many programming systems, the user can interactively construct a program by repeatedly triggering a completion mechanism and choosing one of the offered options. This is the case with code editors for object-oriented languages (choosing a member), data exploration environments (choosing a transformation), but also with theorem provers (choosing a tactic) and structure editors (choosing a grammar~rule). We capture the essence of this interaction pattern through a small formal model called the choose-your-own-adventure calculus. The model serves three roles. First, it reveals subtle differences between instances of the interaction pattern. Second, it enables transfer of interaction techniques across different domains by describing them abstractly in terms of the calculus. Examples include mixed-initiative interaction, AI assistants and programming by demonstration. Third, it lets us characterise desirable properties of a programming system, including correctness, completeness and uniqueness. More generally, the paper shows that programming language theory can be used to study not just languages, but also rich interactive programming systems. We argue that such systems deserve at least as much attention as languages.