Type-Checked Against Nothing
Written later and filed to this date, as part of filling in every day of the year.
The file is five lines long. Four of the lines are a comment. The fifth is declare module followed by the name of the glasses vendor’s software kit, and it tells the type checker that the kit exists and exports anything at all. The commit that added it, at 11:32, explains why: the build had been failing because the code imported a package that was not installed yet. With the stub in place, the build reports what you would hope: typecheck clean, full test suite green.
The project was sixteen minutes old in version control. It is a launcher for my glasses that hosts many small apps at once, one painting the display and all of them ticking, and it had arrived that morning as thirty files and a 368-line spec, promoted from an abandoned worktree where it had been scaffolded and never committed. Its bridge to the glasses was written against a kit that had never been installed. You can see the guessing in the code. Where the bridge subscribes to input, it checks whether the kit has a function called onInput, and if not, whether it has one called onInputEvent.
What followed over the next ninety minutes is four layers of checking, each one green against the layer before it.
Green against a guess
The stub turned off the only check that could have objected. A shorthand module declaration makes every import from that package the type any, so the guessed function names, the guessed shape of a page, the guessed type of an identifier all type-check, because there is nothing to check them against. The comment beside it is candid: the bridge adapts whatever the kit exports, so any is intentional. It was intentional. It also meant the green build was a statement about the project’s internal consistency and nothing else.
Green against the declarations
At noon the real kit was installed, and the bridge was rewritten against its README and its published type declarations. The commit lists what the first version had guessed wrong. It assumed a generic list of containers; the kit wants a descriptor with separate arrays for lists, text and images and a total count. It assumed string identifiers for containers; they are numbers. It assumed an input channel; there is none. Input, lifecycle events and system codes all arrive through one event callback, and the bridge has to split them itself.
That commit ends on a line I wish every commit carried: typecheck clean, thirty-seven tests green, not yet run on the simulator.
Green against behaviour
Twelve minutes later it had been. The vendor ships a simulator that emulates the glasses, and the session drove it one action at a time while reading the kit’s raw event log. Three more things were wrong, and the type declarations could not have shown any of them.
A double press, which the launcher uses for Home, arrives as a system event carrying code 3, not as an input event. A single press on a text container arrives as a system event with no event type at all. The adapter had routed every system event to the lifecycle handlers, so Home was swallowed and text presses vanished.
Scrolling a list produces no event. The firmware moves the highlight itself and tells the app nothing until a press, which then reports the index of whatever is highlighted. The launcher had kept its own selection counter, incremented on scroll events that never come.
And the call that builds the first page may run once per session. A second call, after a reload for instance, returns a code for invalid, and the page stays blank. The fix falls back to the rebuild call.
All three failures are absences: a field that is not there, an event that does not fire, a call that is refused the second time. A type can say a field is optional. It cannot say the field goes missing only when the press lands on one kind of container, and it has no way to describe an event that never arrives.
Green against the next thing down
Forty-five minutes later the image path, wired but never exercised, got its first app, and it had an absence of its own. A focused app was only ever given a text page, so the call that updated image pixels was addressed to a container that had never been built. The fix builds the image page on first use. The commit closes on what the simulator still cannot vouch for: whether the pixels look right, because the simulator re-implements its own drawing, and that check waits for the hardware.
The order of the evidence
None of the checks lied. The stub’s green was true about the code; the declarations’ green was true about the shapes; the simulator’s green was true about an emulation. Each one certified the layer above it against whatever it was given, and each was replaced, within the hour, by one that knew a little more about what the glasses actually do. The mistake would have been to stop at any of them, and the commits show three chances to.
At a quarter past twelve the README had already traded its not-test-verified status for five gates passing on the live simulator, with a new section on what still needs hardware. The five-line stub had been deleted at noon, in the commit that read the real declarations. Its comment had promised exactly that: once the real package is present, its own types take over and this can go.