Typestate Analysis

Every programmer has seen it: a file you forgot to open, a socket you tried to read after closing, a database connection you used after it was freed. The program compiles, it runs, and then — at 3 AM in production — it crashes.

Typestate analysis attacks this class of bugs at the root. The key insight, introduced by Robert Strom and Shaula Yemini in 1986, is simple: encode the current lifecycle state of an object directly into its type. An unopened file has a different type than an open one. A closed connection and an active connection are distinct types. And once states are types, using an object in the wrong state becomes a type error — the kind that the compiler catches before you ever run the program.

This is not just a theoretical nicety. The Rust programming language adopted a close relative of typestate (its ownership and borrow-checker system) as a core design principle, and it is one of the main reasons Rust can guarantee memory safety without a garbage collector. Understanding typestate is understanding one of the most powerful ideas in modern type theory.

A file passes through states: Closed → Open → Closed. Each state allows only certain operations. Build a sequence of operations using the buttons, then press Check to see whether the typestate checker accepts or rejects your program.

<!-- {{c_intro}} -->
<p class="hint">{{hint_para}}</p>
<div class="state-bar">
  <span class="state-label">{{label_state}}</span>
  <span id="state-display" class="state-chip closed">{{state_closed}}</span>
</div>
<div id="program" class="program">
  <span class="placeholder">{{placeholder_empty}}</span>
</div>
<div class="op-buttons">
  <button id="btn-open" type="button" title="{{title_open}}">open()</button>
  <button id="btn-read" type="button" title="{{title_read}}">read()</button>
  <button id="btn-write" type="button" title="{{title_write}}">write()</button>
  <button id="btn-close" type="button" title="{{title_close}}">close()</button>
</div>
<div class="action-row">
  <button id="btn-check" type="button">{{btn_check}}</button>
  <button id="btn-reset" type="button" class="ghost">{{btn_reset}}</button>
</div>
<div id="status" class="status"></div>
<div id="trace" class="trace"></div>

/* {{c_css_intro}} */
* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; }
.hint { font-size: .88rem; color: #444; margin: 0 0 .8rem; line-height: 1.5; }
.state-bar { display: flex; align-items: center; gap: .5rem; margin-bottom: .6rem; }
.state-label { font-size: .8rem; font-weight: 600; color: #555; text-transform: uppercase; letter-spacing: .05em; }
.state-chip { font: 700 .82rem ui-monospace, monospace; padding: .18rem .55rem; border-radius: 5px; }
.state-chip.closed { background: #e8eef3; color: #1d3557; border: 1px solid #cdd9e3; }
.state-chip.open   { background: #d4edda; color: #155724; border: 1px solid #b8d9c3; }
.program { min-height: 2.4rem; background: #f5f7fa; border: 1px solid #dce3ec; border-radius: 8px;
           padding: .45rem .65rem; font: .85rem ui-monospace, monospace; display: flex; flex-wrap: wrap;
           gap: .3rem; align-items: center; margin-bottom: .7rem; }
.placeholder { color: #aaa; font-style: italic; font-size: .82rem; }
.op { padding: .2rem .5rem; border-radius: 5px; font: 600 .82rem ui-monospace, monospace;
      display: inline-flex; align-items: center; gap: .25rem; }
.op.ok  { background: #d4edda; color: #155724; border: 1px solid #b8d9c3; }
.op.err { background: #f8d7da; color: #721c24; border: 1px solid #f1b0b7; }
.op .x  { cursor: pointer; font-size: .95rem; opacity: .6; }
.op .x:hover { opacity: 1; }
.op-buttons { display: flex; gap: .5rem; flex-wrap: wrap; margin-bottom: .6rem; }
.op-buttons button { font: 600 .82rem ui-monospace, monospace; padding: .3rem .7rem;
                     border: 1px solid #1d3557; background: #1d3557; color: #fff;
                     border-radius: 7px; cursor: pointer; }
.op-buttons button:hover { opacity: .85; }
.action-row { display: flex; gap: .5rem; flex-wrap: wrap; margin-bottom: .5rem; }
.action-row button { font: 600 14px system-ui, sans-serif; padding: .4rem .9rem;
                     border: 1px solid #1d3557; background: #1d3557; color: #fff;
                     border-radius: 8px; cursor: pointer; }
.action-row button.ghost { background: #fff; color: #1d3557; }
.status { font-size: 1rem; font-weight: 600; min-height: 1.4em; }
.status.ok  { color: #0a7d33; }
.status.err { color: #c92f3c; }
.trace { font: .8rem ui-monospace, monospace; color: #555; margin-top: .4rem; line-height: 1.6; white-space: pre-wrap; }

// Code not found

Notice the asymmetry. Checking whether a sequence is valid is linear — walk the states one step at a time. But writing a correct program means respecting the protocol in every execution path, including branches, loops, and error handlers. That is the hard part that typestate analysis automates.

How hard is typestate analysis, really?

• Checking one path is trivial: start at the initial state, apply each operation in sequence, reject if any step is illegal. This is $O(n)$ in the length of the program.
• All paths matter. Real programs have branches, loops, and exceptions. A method called inside an if might leave the object in a different state along different branches. The checker must track all possible states the object can be in at each program point — this is a dataflow analysis problem.
• Finite state machines. If the object's lifecycle is modeled as a finite automaton with $k$ states, the analysis propagates sets of possible states through the control-flow graph. With $n$ program points, the fixpoint computation runs in $O(n \cdot k)$ time — polynomial and practical.
• Undecidability at the edges. If you allow the state to depend on runtime values (for example, the file is open if and only if a boolean flag is true), the analysis becomes intertwined with general dataflow, which is undecidable for arbitrary programs. Real tools either restrict the model or use sound approximations.
• Alias analysis is the hard part. Two variables can point to the same object. If you open it through one alias and close it through another, a naive typestate checker is confused. Handling aliasing correctly — as Rust does with its borrow checker — requires solving problems related to pointer analysis, which is itself PSPACE-hard in full generality.

The result is a practical sweet spot: for the common case (single-owner, sequential state transitions), typestate checking is fast and exact. For full generality with aliasing and concurrency, it shades into the hard problems of program analysis.

Typestate is not an academic curiosity — it is one of the most practically impactful ideas in type theory:

• Rust's ownership system: Rust does not have a garbage collector. Instead, every value has a single owner, and the borrow checker enforces at compile time that you never use a value after it has been moved or dropped. This is typestate in disguise: T, &T, &mut T, and the dropped state are distinct types that the compiler tracks through the program.
• Network protocols: a TLS connection goes through states — handshaking, established, shutdown. Encoding those states in types (as the rustls library does) means you cannot call send() before the handshake completes — the type simply does not have that method.
• Embedded and systems programming: hardware peripherals (UART ports, DMA channels) have precise initialization sequences. Typestate lets you model "peripheral is initialized" vs. "peripheral is uninitialized" as different types, so the driver cannot be misused.
• Cryptographic APIs: many vulnerabilities come from using a cipher object in the wrong phase — before a key is set, after finalization. Typestate-enforced APIs eliminate the whole category.
• Database transactions: a Transaction type that transitions from Active to Committed or Rolled Back prevents double-commit bugs statically.

In all of these cases the benefit is the same: bugs that would surface at runtime — or only under specific timing conditions — become compile-time errors that cannot ship. The cost is a richer type system and sometimes more verbose code; the reward is a whole class of production incidents that simply cannot happen.

Typestate analysis is a beautiful marriage of two fundamental ideas: finite automata (the lifecycle of a resource is a state machine) and type theory (wrong states should be type errors). The result is that an entire category of runtime bugs — use-after-close, double-free, missing initialization — becomes structurally impossible rather than merely unlikely.

The most important production of this idea is Rust, where the ownership and borrow-checker system enforces typestate discipline for every value in the program, not just explicitly annotated resources. That is why Rust can promise memory safety without a garbage collector: the type system itself carries the proof.

The next time you see a Rust compiler error that says "value used after move," you are not looking at an annoying restriction. You are looking at a type error that, in any other language, would have been a segfault waiting to happen at 3 AM.