Technology should not aim to replace humans, rather amplify human capabilities.
– Douglas Engelbart, 1958
Programming is an iterative cycle of code edits and feedback until the program behavior matches the intended behavior
Live programming environments improve this feedback cycle by enabling programmers to edit the code of running programs and obtain immediate feedback
Check whether multiple specifications are consistent with each other and provide feedback about discrepancies
An art or music performance in front of an audience (see e.g. Sam Aaron and Ben Smith)
Patching running systems with explicit state migrations (see e.g. Michael Hicks and Scott Nettles)
Environments with integrated development tools and runtime code updates (see e.g. Squeak Smalltalk)
Runtime code updates during the development process with explicit emphasis on immediate feedback (see e.g. Elm Debugger)
If there is any delay in the feedback loop between thinking of something and seeing it, then there is this whole world of ideas which will never be.
– Bret Victor
1
2
3
4
5
6
7
8
9
<span id="val">Count: 0</span>
<button id="incButton">+</button>
<script>
var count = 0;
$("#incButton").on("click", function () {
count++;
$("#val").html("Count: " + count);
});
</script>
Problem: No live feedback for changes due to the structure of the code
let count = 0;
function view() {
return (
<div>
Count: {count}
<button onclick={inc}>
Inc!
</button>
</div>);
}
function inc() {
count++;
}
String literals in the source code are wrapped in transparent proxies that track string origin information
let x = "ab"; x: [ ("ab", 9) ]
let y = x + "c"; y: [ ("ab", 9), ("c", 16) ]
let z = y[1]; z: [ ("b", 10) ]
More complex programming-by-example introduces ambiguities
Check whether multiple specifications are consistent with each other and provide feedback about discrepancies
typeof
operator can be used
function max(a, b) {
requires(typeof(a)=="number");
requires(typeof(b)=="number");
ensures(result => result >= a);
if (a > b) {
return a;
} else {
return b;
}
}
$ \wedge~~~~a > b~\Rightarrow~result\negmedspace=\negmedspace a$
function sumTo (n) {
requires(Number.isInteger(n));
requires(n >= 0);
ensures(res => res === (n + 1) * n / 2);
let i = 0;
let s = 0;
while (i < n) {
invariant(Number.isInteger(i));
invariant(Number.isInteger(s));
invariant(i <= n);
invariant(s === (i + 1) * i / 2);
i++;
s = s + i;
}
return s;
}
function max(a, b) {
requires(typeof(a)=="number");
requires(typeof(b)=="number");
ensures(result => result >= a);
if (a > b) {
return a;
} else {
return b;
}
}
const x = max(23, 42);
assert(x >= 23);
$ \forall x. $
$ ~~~~ ( \forall a, b.~( $
$ ~~~~~~ \texttt{typeof}(a) = \texttt{"number"} ~\wedge~ $
$ ~~~~~~ \texttt{typeof}(b) = \texttt{"number"} ~\Rightarrow~ $
$ ~~~~~~ max(a, b) \ge a ) ) $
$ \wedge ~~~~ x = max(23, 42) $
$ \Longrightarrow x \ge 23$
function inc (x) {
requires(Number.isInteger(x));
ensures(y => Number.isInteger(y) && y > x);
return x + 1;
}
$ \forall x. \{ call(x) \} \Rightarrow $
$ \left( isInt(x) ~\Rightarrow~pre(\texttt{inc}, x) \right) ~\wedge~ \left( isInt(x) \wedge \,post(\texttt{inc}, x)~\Rightarrow~ \texttt{inc}(x) > x \right)) $
function inc (x) {
requires(Number.isInteger(x));
ensures(y => Number.isInteger(y) && y > x);
return x + 1;
}
const y = inc(23);
assert(y > 23);
$ \forall y. $
$ ~~~~~~ \left( \forall x. \{ call(x) \} \Rightarrow \left( ...~\Rightarrow~pre(\texttt{inc}, x) \right) \wedge~ \left( ... \wedge \, post(\texttt{inc}, x) ~\Rightarrow~ ... \right) \right) $
$ \wedge ~~~~ call(23) $
$ \wedge ~~~~ post(\texttt{inc}, 23) $
$ \wedge ~~~~ y = \texttt{inc}(23) $
$ \Longrightarrow y > 23 $
function inc (x) {
requires(Number.isInteger(x));
ensures(y => Number.isInteger(y) && y > x);
return x + 1;
}
const y = inc(23);
assert(y > 23);
$ \forall y. $
$ ~~~~~~\, \left( isInt(23) ~\Rightarrow~pre(\texttt{inc}, 23) \right) $
$ \wedge~~~~ \left( isInt(23) ~\wedge~post(\texttt{inc},23)~\Rightarrow~ \texttt{inc}(23) > 23 \right) $
$ \wedge ~~~~ post(\texttt{inc}, 23) $
$ \wedge ~~~~ y = \texttt{inc}(23) $
$ \Longrightarrow y > 23$
function inc (x) {
requires(Number.isInteger(x));
ensures(y => Number.isInteger(y) && y > x);
return x + 1;
}
function twice (f, n) {
requires(spec(f, (x) => Number.isInteger(x),
(x,y) => Number.isInteger(y) && y > x));
requires(Number.isInteger(n));
ensures(res => res >= n + 2);
return f(f(n));
}
const m = twice(inc, 3);
assert(m >= 5);
class Adder {
constructor (base) {
this.base = base;
}
invariant () {
return Number.isInteger(this.base);
}
addTo (n) {
requires(Number.isInteger(n));
return this.base + n;
}
}
$ \forall x. \{ access(x) \} \Rightarrow \left( ~x ~~\texttt{instanceof} ~~ \texttt{Adder} ~\Rightarrow~ isInt(x.base) \right) $
About 50-80% of source code are verifier annotations
$T \in \text{Types} ~::=~ \{~x: B~|~ R~\} ~|~ x:T \rightarrow T \hspace{2.5em} B ~::=~ \text{Bool}~|~ \text{Int}$
spec
Response (%) | Verification Inspector | Counterexample Popups | Integrated Debugger |
---|---|---|---|
Helpful | 33 | 55 | 44 |
UI Issues | 50 | 39 | 44 |
Not useful | 6 | 6 | 6 |
Impairs development | 11 | 0 | 6 |
To improve our collective ability to solve the world’s problems, we must harness the immense promise and power of technology.
– Douglas Engelbart
Response (%) | Verification Inspector | Counterexample Popups | Integrated Debugger |
---|---|---|---|
Used this feature in experiments | 39 | 50 | 28 |
Unsuccessfully tried using it | 33 | 33 | 22 |
Did not use it | 27 | 17 | 50 |