I designed a new small feature for TanStack DB yesterday and I thought it was a nice snapshot of where I/we are at with AI-enhanced software design. My process is dramatically different and faster than it was pre-ai. Coming up with something this sophisticated would have taken a lot more research/prototyping time in the past.
With my Field Lab skill, I've moved deeply into structured analysis (with what I call "linguistic algorithms") which I find very satisfactory and I think the results are much better than what I used to get.
The process of coming up with this took maybe 20-30 minutes of active time and ~3 hours of agent time.
https://github.com/TanStack/db/issues/1935
I had the agent write up a summary of what we did
How we got to this design
We started from a real app's hand-built subscription manager and asked what TanStack DB should provide instead. We didn't go straight to an API. We ran a series of structured steps. Each one looked at the problem in a different way and checked the step before it.
-
Survey. We looked at how other libraries and apps tie live event channels to cached query data. We noted what they get right and where they break.
-
Lifecycle model. We described the problem as a short list of states and actions: acquire, release, fetch, event, evict and cleanup. Then we generated many orderings of those actions. This found edge cases that are easy to miss by hand, such as an event arriving while a fetch is in flight, or a user leaving during a fetch.
-
Candidate designs. We combined the findings into full designs over three rounds. After each round we checked that nothing had been dropped and that no two parts contradicted each other. We then wrote four different candidate designs and compared them side by side.
-
Decisions. Kyle chose among the options:
- Events can write rows directly.
- A channel lives exactly as long as its Query stays in the cache (gcTime), with no separate setting.
- Sharing one socket among many listeners is the app's job, not the library's.
- Refetch hints are a supported option, with debouncing.
-
Stress test of the chosen design. We wrote the design's rules down and tried to break them with hostile cases, such as late events, stale fetches, and rows shared by two subsets. Each break either changed a rule or became a documented limit.
-
Formal model (TLA+). We encoded the design and had a model checker try every ordering of events for two subsets that share a row. It found four rules the design needs:
- an event marks every Query that holds the row as out of date, including cached ones;
- on a shared row, the newer fetch wins;
- a direct write to a shared row makes the other subset refetch;
- the first fetch waits until the server confirms the subscription.
To show the model can catch real mistakes, we also removed each safeguard in turn and checked that the model then reported the matching failure. The model also found a race that exists in TanStack DB today, with no subscriptions involved.
-
Final check against the original. We compared the draft issue with the original manager's code line by line. This recovered cases the draft had dropped and fixed contradictions before we published.
The result is issue #1935. It includes the formal model, which can serve as the starting point for the test suite when the feature is built.