Chapter 2 · Part I

A Persistent Task Tracker

Chapter 1's contracts guarded values that lived and died within a single run. This project's tasks have to survive being written to disk, closed, and read back, sometimes by a version of the program that no longer agrees with the file format it wrote a year earlier.

tasks_cli is a small, interactive task tracker: add a task with a priority, list them, mark one done, remove one, and have all of it still be there the next time the program starts. Nothing here is algorithmically hard either. The difficulty this project takes on is a different kind: state that outlives the process holding it, and a file format that has to be free to change without every previously saved file becoming garbage the moment it does.

Problem

Unlike Chapter 1's one-shot nexwc, a task tracker used across a session wants a running conversation, not a single argv line — add 3 buy milk, then list, then done 1, all against the same in-memory store, saved to disk after anything that changes it:

tasks_cli — commands: add <priority> <text>, list, done <id>, remove <id>, quit
> add 3 buy milk
added #1
> add 1 write chapter
added #2
> done 2
marked #2 done
> list
[ ] #1 (p3) buy milk
[x] #2 (p1) write chapter
> quit

So the interface here is a REPL loop reading from stdin (Console.read_line) rather than a single parsed argv. This is a better fit for this project on its own terms — a tracker meant to run add, list, and done across one session has no natural single command line to parse. It is the same boundary-parsing discipline as Chapter 1, applied to a line of stdin instead of an argv entry: turn untrusted text into a validated command, once, at the edge, and let everything behind that edge trust the result.

The harder boundary in this project is not the command line at all. It is the file on disk. What gets written today has to still be readable months from now, even after the schema has grown a field that did not exist when some of the saved files were written.

Design as Contract

A task's status is a closed set of two states, and Nex's union makes that fact checkable rather than a convention someone has to remember:

union Task_Status
  Open
  Done
end

There is no string to misspell and no boolean whose meaning is only in a comment. If a third status ever joins Open and Done, every match like this one stops compiling until it accounts for the new case:

is_done(): Boolean do
  match status of
    when Done then result := true
    when Open then result := false
  end
end

Priority takes the same idea further, onto a plain Integer: a task's priority is only ever meaningful between 1 and 5, so that constraint is written once, as the type itself, rather than re-checked at every place a priority value is accepted:

declare type Priority = Integer where p: p >= 1 and p <= 5

Task.make takes a Priority, not an Integer plus a comment saying "must be 1–5" — the type checker enforces the range at the constructor's boundary, and every method inside Task that reads priority back out gets to assume the range holds, because there is no way to construct a Task that violates it. This is the same "parse, don't validate" instinct as Chapter 1's parse_top_count, pushed one level further: instead of a function that checks a condition and returns a plain value, the value's own type carries the condition, and the check happens exactly once, wherever a Priority first comes into existence.

The collection itself, Task_Store, states its promises the same way. Adding a task is guaranteed to grow the collection by exactly one:

add(text: String, priority: Priority): Integer
require
  non_empty: text /= ""
do
  let t: Task := create Task.make(next_id, text, priority)
  tasks.add(t)
  result := next_id
  next_id := next_id + 1
ensure
  grew: tasks.length = old tasks.length + 1
end

old tasks.length is doing real work in that postcondition: it names the collection's size before this method ran, so the ensure clause can state a relationship between two moments in time — not just "the length is some value" but "the length grew by exactly one" — in one line, checked automatically on every call.

One more design decision looks, at first, like the kind of thing a reader might expect to be a mistake: add returns the new task's id, an Integer, not the Task object it just created. A caller holding an id has to go back through find to get anything, which keeps Task_Store the single place that can tell you a task's current, authoritative state; a caller holding a direct reference to a Task object could let it go stale the moment the store's own copy changes underneath it.

Build

Source

The complete, current code for this project is at examples/contracts_at_work/02_task_tracker on GitHub.

Task_Store keeps serialization and file I/O as two separate concerns on purpose: to_json/parse_json touch nothing but strings and are testable without a filesystem; save_to/load_from are the only two methods that know a Path exists at all.

The interesting design decision is the file format itself. The current schema (version 2) writes one JSON object per line (a header line naming the schema version, then one line per task) rather than a single document with a nested array:

{"schema_version":2}
{"id":1,"text":"buy milk","priority":3,"status":"open"}
{"id":2,"text":"write chapter","priority":1,"status":"done"}

A flat, one-record-per-line format is easy to append to and easy to diff, a reasonable choice for a store that saves after every change, independent of anything the language does or doesn't do well. Reading it back has to handle two schema versions at once, because task files written before this project's schema grew a priority field, and used a plain boolean instead of an open/closed status, still have to load correctly:

-- schema version 1: one JSON document, a bare top-level array:
-- [{"id":1,"text":"...","done":false}, ...]
if trimmed.starts_with("[") then
  let items: Array[Any] := json.parse(trimmed)
  ...
else
  -- schema version 2: one JSON object per line; skip the header line.
  let lines: Array[String] := trimmed.split("\n")
  ...
end

Whichever branch runs, both funnel into the same reconstruction step, where the two schemas' differences get resolved once, in one place, rather than scattered through the rest of the class:

let priority: Integer := m.try_get("priority", 3)
let done: Boolean := false
if m.contains_key("status") then
  done := (m.get("status") = "done")
elseif m.contains_key("done") then
  done := m.get("done")
end

A version-1 file with no priority field gets a sensible default (3) rather than a missing-field error; a version-1 file's boolean done and a version-2 file's string status both resolve to the same internal Task_Status. Migration happens once, at load, and everything downstream — including every method on Task — only ever sees the current shape.

Test

Eighteen checks cover the store's ordinary operations — add, find, mark_done, remove, and the failure cases (marking a nonexistent id, removing twice) — plus two that exercise persistence directly, without touching disk. A round trip through to_json and back through parse_json confirms the format preserves everything that matters:

let json_text: String := store.to_json()
let reloaded: Task_Store := create Task_Store.make()
reloaded.parse_json(json_text)
c.check("round trip task text", "write chapter", reloaded.tasks.get(0).text)
c.check("round trip status survives", "true", "" + reloaded.tasks.get(0).is_done())
c.check("round trip priority survives", "1", "" + reloaded.tasks.get(0).priority)

And a hand-written schema-version-1 string, constructed directly in the test rather than loaded from a fixture file, confirms migration works without ever writing an old-format file to disk first:

let legacy_json: String := "[{\"id\":5,\"text\":\"legacy task\",\"done\":true}," +
"{\"id\":7,\"text\":\"legacy open task\",\"done\":false}]"
let migrated: Task_Store := create Task_Store.make()
migrated.parse_json(legacy_json)
let m5: ?Task := migrated.find(5)
...
c.check("migrated default priority", "3", "" + m5.priority)
c.check("migrated next_id", "8", "" + migrated.next_id)

That last assertion — next_id correctly picking up at one past the highest id seen, even across a migrated file whose ids were never assigned by this store's own counter — is the kind of edge a manual smoke test tends to miss and an automated check catches for free, every time, forever.

Takeaways

A closed set of states is worth writing as a union, and a bounded number is worth writing as a refinement type, rather than either becoming a comment asking a future reader to remember a rule by hand. Both put the checking where the type checker can do it once, instead of at every place the value gets used. A method that returns an id instead of a direct reference keeps one object the single, authoritative source of an entity's current state; a caller holding a direct reference can end up trusting a copy that has already gone stale. And when a stored format has to change, handle every version's differences in exactly one place, at load — parse_json here — so that everything downstream, including every method on Task, only ever has to reason about the current shape.

Chapter 3 turns to a simpler kind of state, one that never has to survive being written to disk at all, and asks what's left to say about a contract once persistence isn't part of the problem.