Visibility is Verification
When generation is cheap, the scarce skill is seeing what the code actually did
Table of Contents
- 1. Thesis: you verify by seeing
- 2. The new priorities are visibility instruments
- 3. Three findings: you could not verify it until you could see it
- 4. Survey: making the invisible visible, across paradigms
- 5. Time-travel as the history axis
- 6. Related work
- 7. Coda: the container is the claim
- 8. References
- Seen at
1. Thesis: you verify by seeing
The organizing claim of this line of work has been: cheap generation makes verification the scarce discipline. When producing a candidate — code, a patch, a design — is nearly free, the binding constraint is no longer making it; it is knowing which candidates are correct. System reliability is bounded by the verifier, not the generator.
You verify by seeing, not reasoning. Reasoning about whether code is right is itself a form of generation — it produces a plausible story. Verification is observation: running it, and looking at what actually happened. And observation of a running system is exactly Bret Victor's demand that a creator have an immediate connection to what they make — that behavior, flow, and state be made visible rather than simulated in the head (Victor 2012a, 2012b).
Cheap generation makes verification scarce; you verify by seeing; therefore cheap generation makes visibility scarce — the valuable tooling shifts from helping you write (autocomplete, codegen) to helping you see what the written thing does. The generator emits plausible-looking wrongness at scale; only surfacing the actual runtime state catches it. The expensive failures are the silent ones — the run that returns a believable result instead of an error — and the silent failures live precisely in the state you cannot see.
2. The new priorities are visibility instruments
Under cheap generation the shopping list changes. What is worth building, buying, or handing an agent is the set of instruments that make some layer of the system visible enough to verify. They sort by which layer they expose and at what granularity — a point, a flow, or a history.
| instrument | layer exposed | makes visible | exemplar |
|---|---|---|---|
| tests (property-based) | the oracle | is it correct | QuickCheck (Claessen and Hughes 2000) |
| code index (LSP / AST search) | static structure | who-calls, relationships | Language Server Protocol; tree-sitter |
| diagram / flow analysis | static + control flow | the shape | control-flow / dataflow graphs |
| debugging | runtime state at a point | the value here, now | SLDB; rr (O’Callahan et al. 2017); FlowStorm |
| log visibility / telemetry | behavior over time | what happened, in aggregate | OpenTelemetry; Erlang :observer |
| system tracing | flow across components | the causal path | distributed tracing; DTRACE |
| context (the rendered artifact) | the output itself | the real thing, not a proxy | browser DevTools DOM inspector |
The rendered artifact is not its telemetry. The most under-served instrument is the one that shows the thing itself — the rendered DOM, the actual image, the real output — rather than logs or execution telemetry about it. Telemetry is a lossy projection chosen in advance; verification often needs the artifact unprojected. For an autonomous agent this is decisive: to verify a UI change it must see the render, not infer it from a log line.
Static and dynamic are both visibility. A code index (LSP, an AST-level search, a call graph) makes structure visible before anything runs; a tracer makes behavior visible after. Both are the same act at different times — turning an invisible relationship into something you can look at.
3. Three findings: you could not verify it until you could see it
These came out of a literate rebuild of a Common Lisp textbook under a current toolchain — the pedagogy testbed for this program. Each is a small, reproducible instance of the thesis: invisible state hid a fact, and surfacing it settled the question.
3.1. The read-time package: silent wrongness in the gap between reading and evaluating
re-reproduced on SBCL 2.6.3: (read-from-string "(progn (in-package :zzpkg) (defun f (x) x))") evaluated with *package* bound to CL-USER defines F in CL-USER -- (fboundp (find-symbol "F" :cl-user)) -> the function, and (find-symbol "F" :zzpkg) -> NIL, status NIL (no F symbol in :zzpkg at all). Confirms the full-progn read happens before in-package runs, on a different SBCL release than the original pass. Claim precisely correct.
Evaluating (progn (in-package :a) (defun f …)) defines f in the wrong
package. The reader interns every symbol in the progn before in-package ever
evaluates, so f lands wherever *package* pointed when the form was read — not
where in-package moves it. No error; a plausible, wrong result. The fix is to
bind *package* before the read (which is what a :package argument to the
evaluator does). The point is not the fix; it is that reasoning about the code
says "obviously it goes in :a," and only running it — making the binding
visible — says otherwise.
3.2. The detangle "failure" was a measurement artifact
confirmed via emacs -Q --batch (GNU Emacs 30.2): (default-value 'org-babel-tangle-use-relative-file-links) -> t, so real trees emit RELATIVE links, not absolute ones. Body corrected 2026-10-08 from "real trees emit absolute links" to "real trees emit relative links by default ... because the layout stays stable, not because the links are absolute" (prior pass's proposed reword, now applied).
A documented failure — that org-mode's tangle/detangle round-trip does not survive — turned out, on re-running, to be a sandbox relocating files and invalidating relative link comments. Real trees emit relative links by default and round-trip cleanly anyway, because the layout stays stable, not because the links are absolute. The lesson is verification applied to your own prior negative result: a red result is data about the harness until you have looked at why it is red. Believe the run, not the reasoning — including your own earlier reasoning that produced the "failure."
3.3. Traces as regenerated, verified artifacts — documentation that cannot rot
sound as a literate build-oracle design (definitional), but the empirical drift-fails-the-build behavior shows no reproducible artifact in this note.
A recursion's execution trace, embedded in the prose as a figure, is generated from the tangled code and re-checked on every build; if the code drifts, the build fails. The transcript is the primary artifact, not a pasted REPL session that quietly goes stale. This is literate programming meeting the oracle: the visible artifact and the verified artifact are the same object.
4. Survey: making the invisible visible, across paradigms
both prior-pass errors confirmed against primary sources and fixed in survey.org. (1) rubygems.org API: https://rubygems.org/api/v1/gems/pry-timetravel.json resolves (gem "pry-timetravel", Brock Wilcox); .../pry-time-travel.json returns "could not be found" -- table corrected to pry-timetravel. (2) rr's own README (raw.githubusercontent.com/rr-debugger/rr/master/README.md): "a lightweight tool for recording, replaying and debugging execution of applications" on Linux via ptrace, no Rust affiliation -- rr is already cited generically in the taxonomy table above (#taxonomy), so the Rust row's "; rr (record/replay, reverse-step)" clause is dropped as a miscategorized duplicate. core.memoize snapshot/memo-clear! and :ets.tab2list/1 unchanged from prior pass.
Every ecosystem has grown the same two-move pattern — a pipe that emits hidden state and a renderer that draws it — and the mature libraries expose runtime state as plain data on purpose.
The split is cleanest in Clojure: tap> is a language primitive whose only job
is to hand a value to whatever is listening, and Portal, Reveal, and
FlowStorm are interchangeable listeners. Decoupling emit from render is the
lesson to steal.
| ecosystem | the pipe (emit) | the renderer (draw) |
|---|---|---|
| JS / DevTools | console.log/table/dir |
DevTools inspector; Redux DevTools (time-travel over state) |
| Clojure | tap> (a built-in global pipe) |
Portal, Reveal, REBL; FlowStorm (omniscient); pprint/print-table |
| Common Lisp | TRACE, DESCRIBE |
INSPECT + the SLIME inspector (an interactive object browser); SLDB |
| Ruby | TracePoint (call/return/line hooks), pp |
Pry (cd~/~ls into objects); pry-timetravel steps back |
| Rust | dbg!; the tracing crate (spans+events) |
tokio-console (live async tasks) |
| Haskell | Debug.Trace; GHCi :trace / :hist |
ghc-vis — draws thunks, sharing, and forcing without evaluating |
| Elixir / BEAM | dbg/2; :sys.get_state |
:observer — live processes, message queues, ETS tables |
Two entries carry disproportionate weight for the argument. Haskell is the
hard case: laziness makes state genuinely invisible — a thunk is a promise, not a
value — and ghc-vis draws the heap including unforced thunks, so you watch
evaluation happen; nothing else here shows the shape of what has not run yet.
Elixir/BEAM was built introspectable for live systems: :sys.get_state reaches
into any running process and returns its state, and :observer shows ETS
contents live — "see the running system" as a platform feature, not a bolt-on.
The cache thread closes the loop. Memoization is the miniature: the cache is
the invisible state, and the mature libraries expose it on purpose — Clojure's
core.memoize ships snapshot (the cache as a plain map at an instant) and
memo-clear!; Elixir memoizes with ETS, whose :ets.tab2list/1 is the cache as
a visible table. Expose the state as data, then render it. For a recursive fib
the snapshot is the trace, spatially.
5. Time-travel as the history axis
thesis is conjecture (correctly marked :STATUS: speculative); tool descriptions (FlowStorm omniscient, rr record-replay reverse, Redux DevTools time-travel) are factually correct.
Speculative — a conjecture about where the history axis of visibility becomes tractable, not a settled claim.
Debugging shows state at a point; tracing shows a flow; time-travel debugging
shows the whole history, scrubbable. FlowStorm for Clojure, rr's
record-and-replay (O’Callahan et al. 2017), and Redux DevTools are the mainstream
realizations of Victor's "make time visible." The miniature already appears in
the findings above: a memoized function's cache filling 0,1,…,n bottom-up is a
micro-time-travel — the table is the history of the computation. Where this
connects to the repl-driven forking work is the open question: a REPL
session's fork tree and a debugger's replay history are the same structure seen
from two directions.
7. Coda: the container is the claim
This research corpus already practices the thesis on its own prose: headings
carry :CUSTOM_ID: so skeptic and claim-validator agents can attach
:VERIFIED_AT: / :VERDICT: / :FINDING: drawers, and disputed claims are marked
rather than buried. That review apparatus is visibility-is-verification applied
to argument — a claim you can see the verdict on is a claim you can trust.
8. References
all 9 bib entries verified against primary sources; 4 cited keys resolve; 5 orphans intentionally uncited (reading-list).
Seen at
- SPLASH/ISSTA 2026 — Unlocking Safe Agentic Autonomy through Verification, The Checkability Boundary, and the debugger-visualization talks.
- Clojure/Conj 2026 — Patrick de Kruif's source inspector and Juliana Prieto's production traces in the REPL: knowing by seeing.
- Atlassian Team '26 Europe: Closing the context gap — "verified delivery" with verification evidence attached to the Jira work item.
- Atlassian Team '26 Europe: The SDLC, upgraded — the claim that AI gains plateau because tools optimize the share of the day spent writing code.
- Boston AI Week 2026: AI Software Factory with a Human in the Loop — Eli Whitney's staged interchangeable-parts demonstration: a demo taken as proof, the failure this note's instruments are meant to catch.