Tau Language (invariants first, then execution)

This tutorial is about a shift in how to think about writing programs. Once the idea clicks, Tau starts to feel much less alien.

Tau is not imperative code with odd punctuation. It is a declarative language for typed input and output streams.

Instead of giving a step-by-step recipe (“do this, then do that”), a Tau spec says how current and earlier stream values may relate over time. If the spec is satisfiable in Tau’s execution sense, Tau can run it step by step: read the current inputs, solve for the current outputs without peeking at future inputs, advance time, repeat.

One careful point matters from the start. A Tau specification usually denotes a set of possible programs, not just one program. When that set is non-empty, Tau executes one deterministic representative from it.

That can sound a bit slippery on first contact, so this tutorial starts with a concrete habit: before writing any code, write a list of sentences that are meant to stay true forever. Those sentences are your invariants. Everything else, such as syntax, types, and stream declarations, is just scaffolding to make the invariants executable.

All examples in this tutorial are runnable from files under examples/tau/. Each file is a self-contained transcript that runs end-to-end without manual typing.

Part I: inside your head (invariants before syntax)

Imagine designing a turnstile at a subway entrance.

You do not start by writing code. You start by stating what must always be true:

1. The turnstile is always in one of two states: Locked or Unlocked.
2. Inserting a coin when locked unlocks it.
3. Pushing through when unlocked locks it again.
4. Pushing through when locked triggers an alarm.
5. No alarm when unlocked.

These are your invariants. They do most of the real design work before a keyboard even enters the story. They say what the state is, what inputs exist, and what must never be violated.

This is the habit that makes specifications readable: invariants first, then syntax.

Why start with invariants?

When the starting point is syntax, it is easy to get trapped in details: “What type is this? How is that declared? Why is the compiler unhappy already?”

When the starting point is invariants, orientation comes first. The invariants are the spec. Everything else exists to make them checkable.

Part II: reading Tau (the practical version)

Tau is easiest to read if it is pictured as a row of time-stamped boxes. That picture may feel almost too simple, but it really does carry a lot of the tutorial.

A stream is just a sequence of values indexed by time. Think of it like frames in a film, numbered 0, 1, 2, 3, …

• Input streams (i1, i2, …) receive values from the outside world.
• Output streams (o1, o2, …) produce values computed by the spec.

At each time step t, the spec relates inputs and outputs. In Tau, t is not “the current loop counter.” It is a placeholder that means “for every step like this one.”

Declaring streams

i1 : bv[8] := in console   # input stream, 8-bit values
o1 : bv[8] := out console  # output stream, 8-bit values

Writing constraints

In the fragment used on this page, a top-level Tau spec is a formula. The value side is a term, for example o1[t-1] + i1[t]. The full statement is a formula, for example o1[t] = o1[t-1] + i1[t].

A common beginner pattern is a formula that relates values at the current time step, and sometimes earlier steps too:

o1[t] = o1[t-1] + i1[t]

Plain English: “take the old value, add the new input, and that gives the new value.” That is just a running sum. This is a good example of a Tau line that looks more forbidding than it really is.

How to read t-1 and t-2 (unroll it)

The safest way to read Tau is to stop being abstract for a moment and plug in actual numbers. This is worth doing often. Tau gets friendlier very quickly once the symbols are forced to commit to one concrete step.

If a spec contains:

o1[t] = o1[t-1] + i1[t]

then the first few instances look like:

o1[1] = o1[0] + i1[1]
o1[2] = o1[1] + i1[2]
o1[3] = o1[2] + i1[3]

That is all t-1 means: “the previous frame.” Similarly, t-2 means “two frames back.” If a constraint uses t-2, unrolling it will show dependencies that skip one step.

Most runnable examples on this page have bounded lookback. That just means the rule for step t only looks at a fixed finite window, such as t and t-1, or t, t-1, and t-2. This is the recurrence-shaped fragment that feels most like “state update,” even though Tau itself is phrased in streams rather than mutable variables.

If the state-machine picture is easier to hold in mind, read the indices like this:

• o1[t-1]: the state before the transition
• i1[t]: the event/input at this step (the arrow label)
• o1[t]: the state after the transition

Tau writes the transition rule as an equation over these time-indexed values.

The mindset shift

This is the biggest mindset shift in the page:

• An imperative program computes outputs by executing instructions step by step.
• A Tau specification constrains outputs by stating relationships that must hold.

During execution, Tau receives the current inputs and solves for the current outputs in a way that keeps the spec true now and still compatible with continuing later. One good mental model is “fill in the blanks for this step, but only in ways that keep the run extendable.” It is less like writing instructions for a machine to follow, and more like laying down rails and asking for the next legal move.

Part III: the same system in three lenses

The turnstile can be described in three equivalent ways. Nothing about the system changes. Only the notation changes.

Lens 1: state machine (the picture)

Draw circles for states (Locked, Unlocked) and arrows for transitions (coin, push). This is the visual view: good for intuition, but hard to execute directly.

Lens 2: recurrence relation (the function)

Define a step function that takes the current state and event, and returns the next state:

This is the functional view. The whole behavior unfolds from an initial state and repeated application of step.

Lens 3: Tau specification (the constraints)

Encode the state as an output stream, encode the event as an input stream, and write constraints:

• o1[0] = 0 (start locked)
• o1[t] = 1 if coin and not push (unlock)
• o1[t] = 0 if push (lock)
• o2[t] = 1 if push while locked (alarm)

This is the declarative view. For this tiny example, the constraints pin down one behavior. In general Tau can leave several behaviors admissible, then execution picks one deterministic representative. Same turnstile, different accent.

One turnstile step through all three lenses

Take one concrete moment:

• at time t-1, the turnstile is Locked
• at time t, a coin arrives
• at time t, there is no push
• at time t, the next state should be Unlocked

Here is the same event in three forms:

• State machine: Locked --coin--> Unlocked
• Recurrence instance: state_t = step(Locked, coin) = Unlocked
• Tau instance: if o1[t-1] = 0 && coin[t] = 1 && push[t] = 0, then o1[t] = 1

Why three lenses?

Different tools want different representations:

• Humans often prefer state machines (visual, local).
• Recursive code uses recurrence relations.
• Constraint solvers use logic specifications.

The key insight from Tutorial 2 (Isomorphism) applies here: these are not three different systems. They are three equivalent descriptions of the same system. Picking the right lens for your task is a practical skill.

Programs as infinite decision trees

The turnstile rules form a case split: given the current state and event, pick the next state. That is a decision tree.

For code without loops, the tree is finite. For code with loops, the tree is conceptually infinite. It keeps branching forever.

State machines and stream specifications are compact ways to describe infinite unfoldings.

Part IV: cards in Tau (an approximate state tracker)

Tutorial 1 built a precise mental picture of a card counter’s running score. Now let’s see that same system in Tau.

The runnable example is:

examples/tau/card_counting_hilo_state_tracker.tau

From the repo root:

./scripts/run_tau_policy.sh examples/tau/card_counting_hilo_state_tracker.tau

What the spec does

The input stream provides a pre-classified delta: +1, 0, or -1 (encoded as 8-bit values: 1, 0, or 255). The output stream maintains a biased running count.

The core constraint is simple:

That is it. No hidden cleverness. The spec just enforces the update rule.

A useful convention: push parsing out of Tau

Notice that Tau does not classify cards. It receives the already-classified delta. This is a design pattern: keep complex parsing in the host system, let Tau enforce simple invariants.

Why? Tau is good at constraints, not string manipulation. The split keeps both sides clean, and it keeps the spec focused on the part that is actually worth checking.

Part V: a toggle puzzle in Tau (and why XOR is linear algebra)

Now connect back to Tutorial 2’s “puzzle becomes linear algebra” example.

Consider a row of lights that are either on or off. Pressing a button toggles some subset of lights. The puzzle is simple to state and strangely satisfying to solve: turn all lights off.

The insight is that toggling is XOR. A board of lights is a bitvector. Applying a move is:

where $\oplus$ is bitwise XOR.

The runnable example is:

examples/tau/toggle_puzzle_xor_state.tau

Why this matters

XOR over bits is the same as addition in $\mathbb{F}_2$ (the field with two elements). So “toggle puzzle” and “linear algebra over a finite field” are the same structure.

This is the leverage move from Tutorial 2: recognize an isomorphism, then use tools designed for the target domain. A puzzle that looked fiddly by hand becomes crisp once it is seen in the right language.

Part VI: Q-learning as a lookup table (and what Tau can check)

What a lookup table really is

A lookup table is a function on a finite domain, stored as a list of values. There is nothing mystical about it. It is just a very explicit function representation.

For tabular Q-learning, the table maps (state, action) pairs to scores:

If $S$ and $A$ are small and finite, you can literally store every entry. That is a Q-table: a grid of numbers, one per (state, action) pair.

The Q-learning update

The classic update rule is:

In words: blend the old value with a target computed from the reward and the best predicted future value.

For this tutorial, we use a much smaller executable toy. The table entries are bv[8] values, and the update is simplified to target = r + q_next. If learn = 1, the selected entry becomes target.

A runnable Tau example: 2x2 table update

The runnable spec is:

examples/tau/q_learning_tabular_update.tau

Each step provides:

• (s, a): which entry to update (two 0/1 bits)
• r: the reward
• q_next: a stand-in for $\max_{a’} Q(s’, a’)$
• learn: whether to update (0 = no, 1 = yes)
• Q00, Q01, Q10, Q11: the current table entries

The spec computes target = r + q_next and enforces:

• If learn = 1: exactly one entry changes to target; the others stay the same.
• If learn = 0: all entries stay the same.

What Tau gives you

This is the “Tau + lookup table” pattern:

• The host system chooses which entry to update and what the reward is.
• Tau enforces that the update has the right shape.

The combination is powerful because it separates concerns:

• The table is a concrete artifact you can log, diff, and replay.
• The constraints are guardrails: “only this entry updates,” “the update uses this formula.”
• When something breaks, there is a counterexample trace to inspect instead of a vague sense that “training went oddly.”

A note on closing the loop

This spec models a single update step. It takes the current table as input and produces the updated table as output.

To run multi-step learning, the host system must “close the loop”: take the output table and feed it back as the next step’s input. Tau specifies the shape of each step; the host orchestrates the sequence.

Part VII: tables vs weights vs latent space

Lookup tables versus neural network weights

A Q-table represents a function on a small discrete domain. Each entry is one input-output pair.

A neural network also represents a function, but parameterized differently: by weights.

Two questions that sound similar but are not:

1. Expressiveness: Can both representations compute the same input-output behavior?
2. Isomorphism: Is there a 1-to-1, structure-preserving map between them?

For tables and neural networks, (1) can be true. A small network can compute the same function as a table. But (2) is generally false. The map “weights → behavior” is many-to-one: different weight settings can compute the same function.

That is an equivalence relation (same behavior), not an isomorphism (same structure). Same outcome, different internal bookkeeping.

Latent space as a learned abstraction

In deep learning, a latent vector is the model’s internal representation of an input. It is an abstraction: it forgets details while preserving distinctions the model needs.

From the “spaces” perspective:

• State space: all configurations the environment can be in.
• Table space: all possible Q-tables (one coordinate per entry).
• Weight space: all possible neural network parameters.
• Latent space: the internal representation space the model learns.

“Learning” and “verification” are different kinds of search through these spaces:

• Learning searches parameter space for weights that score well on data.
• Verification searches state space for counterexamples that break an invariant.

Running the examples

All examples live in examples/tau/. To run them:

1. Build Tau (once):

   ./scripts/update_tau_lang.sh
   

2. Run an example:

   ./scripts/run_tau_policy.sh examples/tau/turnstile_fsm_alarm.tau
   

Each .tau file is a self-contained REPL transcript: it declares streams, runs the spec, feeds demo inputs, and quits. You can read the file to see both the spec and the expected behavior.

Where this tutorial goes next

This tutorial introduced Tau as a way to write executable specifications. The key habit: invariants first, syntax second.

Next directions:

• Use Tau as a small “logic kernel” inside a larger system: the host computes complex checks, Tau enforces guardrails.
• Connect Tau execution with counterexamples and synthesis loops (CEGIS).
• Build more complex state machines with multiple interacting streams.

If you want to see how constraints connect to learning systems, read Tutorial 4: World Models.