If you come from Elm or Redux

The mapping:

The surprise is that this is the same architecture on the server, with rules and a verifier over every reachable state. A reducer computes the next state from a message; a contract does the same and, in addition, names how it can refuse, keeps an invariant, and is checked from thousands of states it was never sent.

The first program you would write, a todo list:

row Todo { id: id, text: string(64), done: bool }
unit Todos {
    state todos: Todo[16];
    state filter_done: bool = false;
    contract add(todo: id, text: string(64)) {
        case len(text) == 0 => fail Empty;
        else => Added: todos += [Todo { id: todo, text: text, done: false }];
        examples { {} (1, "milk") => Added { todos: [Todo { id: 1, text: "milk", done: false }] }; {} (1, "") => Empty; }
    }
    contract toggle(todo: id) => Toggled: todos[todo].done := !todos[todo].done;
    contract set_filter(done: bool) => Set: filter_done := done;
    contract clear_done() => Cleared: todos -= where(t in todos: t.done).id;
}
flow finish_and_clear(todo: id) atomic { Todos.toggle(todo); Todos.clear_done(); }
view visible() = where(t in Todos.todos: !Todos.filter_done || t.done);
scenario a_list {
    Todos.add(1, "milk") => Added;
    Todos.add(2, "bread") => Added;
    Todos.toggle(1) => Toggled;
    visible() => Value([Todo { id: 1, text: "milk", done: true }, Todo { id: 2, text: "bread", done: false }]);
    finish_and_clear(2) => Cleared;
    visible() => Value([]);
}

scenario a_list
  Todos.add(1, "milk") => Added
  Todos.add(2, "bread") => Added
  Todos.toggle(1) => Toggled
  visible() => Value([Todo { id: 1, text: "milk", done: true }, Todo { id: 2, text: "bread", done: false }])
  finish_and_clear(2) => Cleared
  visible() => Value([])
  Todos = Todos { todos: [], filter_done: false }
6 step(s), all as expected

verify: 2 examples, 6 scenario steps and 8000 sampled checks passed

toggle is the reducer you know, written as a delta. finish_and_clear is two updates in one atomic step, which no reducer can express without a third message. visible is the selector, and the scenario asserts its value directly, so the view is tested with the model.