• A computer is a universal machine that can process any kind of information and perform any kind of computation
• Computation and steps are specified with a programming language
  • very precise and technical
  • unlike natural languages
• Programming is often tedious, frustrating and error-prone!

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

• Live programming
  • Live feedback for graphical applications based on a certain programming style
  • Live programming by example/direct manipulation
• Program Verification
  • Static verification of dynamically-typed JavaScript, including higher-order functions
• Integrated Development and Verification Environments

let count = 0;

function view() {
  return (
    <div>
      Count: {count}
      <button onclick={inc}>
        Inc!
      </button>
    </div>);
}

function inc() {
  count++;
}

• Model holds entire application state
• View generates visible output based on Model
• Update processes events and changes the Model

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

• Need heuristics/ranking or user interactions!

• live programming of the UI code,
• back-in-time debugging, runtime version control and
• live programming by example.

• Live programming
  • Live feedback for graphical applications based on a certain programming style
  • Live programming by example/direct manipulation
• Program Verification
  • Static verification of dynamically-typed JavaScript, including higher-order functions
• Integrated Development and Verification Environments

Check whether multiple specifications are consistent with each other and provide feedback about discrepancies

• Pre- and postconditions, etc. written as standard boolean JavaScript expressions
• Annotations are used for static verification and removed before execution
• Instead of type syntax, the typeof operator can be used
• Need to manually supply loop invariants and other verification hints

function max(a, b) {
  requires(typeof(a)=="number");
  requires(typeof(b)=="number");
  ensures(result => result >= a);

  if (a > b) {
    return a;
  } else {
    return b;
  }
}
 

• Loops and recursion lead to unbound number of paths
• Inferring loop invariants and post-conditions undecidable
• Explicit postconditions and invariants required

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);
 

function inc (x) {
  requires(Number.isInteger(x));
  ensures(y => Number.isInteger(y) && y > x);
  return x + 1;
}
 

• $\{ call(x) \}$ is a trigger pattern
• $pre(\texttt{inc}, x)$ and $post(\texttt{inc}, x)$ uninterpreted function symbols
• $pre(\texttt{inc}, x)$ is satisfied by any integer value for $x$
• $post(\texttt{inc}, x)$ and precondition together imply $\texttt{inc}(x) > x$

function inc (x) {
  requires(Number.isInteger(x));
  ensures(y => Number.isInteger(y) && y > x);
  return x + 1;
}
const y = inc(23);
assert(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);
 

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);
 

• Nested recursive data structures (records, lists, trees)
• Proposed Solution: Simple immutable "classes" with invariants
  • Check invariant when creating instances
  • Instantiate invariant when accessing properties

class Adder {
  constructor (base) {
    this.base = base;
  }
  invariant () {
    return Number.isInteger(this.base);
  }
  addTo (n) {
    requires(Number.isInteger(n));
    return this.base + n;
  }
}

• Reversing an ascending list yields a descending list
• A verified implementation of MergeSort
• A custom list class that can be parameterized by an invariant (somewhat analogous to generics)
• A theorem and proof written in JavaScript showing that any locally increasing integer-ranged function is globally increasing

About 50-80% of source code are verifier annotations

• Pure functional core language with logical propositions as pre- and postconditions

• Verification rules similar to typing rules but also generate verification conditions
• Verification is sound:
  • Verified programs execute without getting stuck
• Verification algorithm is decidable
  • Decision procedure terminates for all inputs
• Complete mechanized proof in Lean

• Refinement types translate to annotations
  • Dependent function types translate to spec
• Conjuecture that well-typed programs translate to verifiable programs
  • Proof is work in progress

• Static program verification can be applied to dynamically-typed JavaScript programs including higher-order functions
• A custom quantifier instantiation ensures that the verification process remains predictable
• Verification is sound and (seemingly) at least as expressive as refinement type systems such as LiquidHaskell

• Live programming
  • Live feedback for graphical applications based on a certain programming style
  • Live programming by example/direct manipulation
• Program Verification
  • Static verification of dynamically-typed JavaScript, including higher-order functions
• Integrated Development and Verification Environments

• Verification issues can be hard to understand and fix due to expressive logic and complex verification procedure
  • Simple error messages inadequate
• Explain verification issues with executable counterexamples (tests)
• An integrated Verification Inspector can show details about a verification issue and enables interactive exploration

• Verification errors can be difficult to understand
• Executable counterexamples and tool integration can assist programmers
• A novel Verification Inspector enables programmers to interactively add or remove assumptions and assertions
• Features are generally seen as helpful by user study participants

• To solve problems with technology, programmers need to communicate the intended program behavior
  • Independent of future advances in artificial intelligence
• Programming is an iterative process
  • Programming environments should aim to provide immediate live feedback for any change to the code
• Static verification enables programmers to specify detailed invariants and check the implementation
  • Interactive tools and environment integration is crucial to make verification usable in practice

• Live programming: Elm, TouchDevelop (especially the It's Alive paper), Jonathan Edwards (including Subtext), and Smalltalk environments such as Squeak and Lively Kernel, everyone at CDG/Y Combinator Research.
• Program Verification: Dafny, LiquidHaskell and Lean
• Finally, thanks to my advisor, Cormac Flanagan, the programming language group at UC Santa Cruz and my PhD committee.