Lambda the Ultimate

I believe this is relevant at least in the context of user studies and end-user programming. In fact, I believe this kind of ideas is relevant in teaching programming to smart people who aren't already (computer) geeks. (I've met some).

I thought of this while answering John Shutt's comment on how Wikipedia's software could evolve — I think it's relevant there (in fact, I find the whole seminar interesting).

I found this paper very interesting, but also a bit hard to read (I found it frustratingly slow-going because I started understanding what precisely was the feature described in the middle of page 4). I will summarize what I understood of the feature, which may help others decide to read the paper, get the TL;DR, and point misunderstandings in my summary.

Setting:

- The feature is designed to encourage non-programmers to add assertion (in fact range constraints) to cells in a spreadsheet.

- The users are debugging formulas in a spreadsheet. The general process is to change the values in the input cells (putting inputs users expect to happen in production use of the spreadsheet), check that the output is what they expect, and otherwise try to identify an error in a formula and fix it. The value of the input cells are not important (they are not real data), users do not try to save them, they just fiddle with them.

- The spreadsheet program displays range constraints (assertions) above each cell, if they are some. It propagates the constraints: if cell A has constraint [1; 3] and cell B constraint [2; 4], and cell C is defined by "= A + B", the program will infer and display the constraint [3; 7].

- When a cell value violate its range constraint, its is highlighted by a red box (but the user is otherwise free to continue playing with the spreadsheet).

Feature: a button "help me test" that users can click. When clicked, the program puts random values in input cells for which the users have provided assertions -- the random value respects the assertion. This provides value for the users, as they can explore the input space (basically, random testing) by repeatedly clicking the button. Additionally (and this is the twist), the program picks an input cell that has no range constraint, guesses a *random* constraint for it, and also picks a value in this range. It is better if the range constraint guessed is recognisably bad, because the aim is to surprise the user and motivate him/her to provide a better constraint.

Additional support: the program keeps track of the provenance of constraints (user-defined, computer-derived, random generated), and shows it to the user. For cells defined by formulas, a red highlight is shown whenever the user-defined range and the computer-derived range are different. This encourages the user to refine the formula (if it is at fault) or fix his/her range. This also reinforces the desire to fix randomly-generated ranges (as they can create mismatches down the way).

Bi-simulation is much more important than assertions because assertions are not very expressive.

Bi-simulation is crucial to auditing in which it is shown that an implementation does everything done by a procedural specification. Ideally, it should also be shown that the procedural specification does everything done by an implementation.