A language made of links

The last article ended in a slightly annoying place. I had a syntax sketch for relationship types: keep fields ordinary, then put the invariant on the edge between them. A packet could say that its declared length and its byte count agree without turning the byte string into Bytes<n>.

That works as an article-sized idea. It is also the easy part. The interesting question is what kind of language you get if you stop treating relationships as a decoration on records and make the compiler care about them everywhere.

Call the language Tether for this sketch. I would keep almost everything else boring: a compiled, eager, expression-oriented language with algebraic data types, local type inference, explicit public signatures, immutable bindings by default, and scoped mutation. The experiment is one thing: values are nodes, relationships are typed links, and the checker knows which links a mutation can break.

A record is a small graph#

The packet from the previous article becomes the first piece of syntax. The fields still have types you would expect in an ordinary systems language. The extra declaration is a named proposition whose endpoints are fields in the same value.

relation SameLength(declared: Nat, bytes: Bytes) =  declared == bytes.lentype Packet = {  length: Nat  body: Bytes  link size: SameLength(length, body)}

I am using link rather than hiding the predicate in one field's type because the compiler needs to remember its shape. size depends on length and body. That dependency is useful information when one of those fields changes.

Links do not have to be binary. An image has a perfectly ordinary width, height, channel count, and byte buffer. The interesting fact only exists because this record puts all four values together.

type Image = {  width: Nat  height: Nat  channels: Nat  pixels: Bytes  link packed:    pixels.len == width * height * channels}

So the internal model is really a hypergraph. Fields are nodes. Every link stores a predicate plus the set of nodes it mentions. That sounds like compiler bookkeeping, because it is. I want the language feature to earn its keep in bookkeeping rather than in prettier theorem syntax.

Construction should usually prove itself#

The first version of relationship types needed an explicit prove while decoding a packet. I would remove that from the common path. Functions can publish small postconditions, and constructing a linked record asks the checker whether the facts already in scope close every link.

fn readExactly(cursor: &mut Cursor, n: Nat)  -> Result<bytes: Bytes, ReadError>  ensures Ok(bytes) => bytes.len == nfn decode(cursor: &mut Cursor) -> Result<Packet, ReadError> {  let length = try cursor.readU16().toNat()  let body = try readExactly(cursor, length)  return Packet { length, body }}

readExactly says that a successful result has exactly the requested length. After the call, the checker has a relationship between length and body, so the Packet literal does not need another comparison and does not need a hand-written proof term.

When the fact really comes from untrusted data, write the check. Flow-sensitive typing can learn from the branch in the same way a null check or tagged-union match teaches many existing type checkers something about the path that follows.

fn Packet.fromParts(length: Nat, body: Bytes)  -> Result<Packet, BadLength>{  if body.len != length {    return Err(BadLength)  }  return Ok(Packet { length, body })}

After the early return, body.len == length is true on the remaining path. That is enough to construct the packet. The check belongs at the boundary; the relationship belongs to the value afterward.

The mutation rule is the language#

This is the part I would actually build Tether to test. Most type-system sketches become much less cute the moment a program wants to update two related fields. If every intermediate assignment must preserve every invariant, simple edits become impossible. If invalid values can float around indefinitely, the invariant is mostly documentation.

My rule would be a scoped hole. An edit block may temporarily break links on the value it owns. The compiler tracks which links become invalid as their endpoints are written, and the closing brace is a proof boundary.

fn truncate(packet: &mut Packet, n: Nat) {  edit packet {    packet.body = packet.body.take(n)    packet.length = packet.body.len  }}

Change body and the size link becomes open. Change length to the new byte count and the checker can close it. If the function forgets the second assignment, the error can be about the relationship that broke instead of some huge inferred type that happens to contain the same fact.

error: cannot finish edit of packet  open link: size  required: packet.length == packet.body.len  packet.body changed here:    packet.body = packet.body.take(n)  packet.length was not updated

More importantly, changing an unrelated field should do nothing to size. The compiler already has the endpoint set for every link. It does not need to re-prove the entire record because a timestamp changed.

Functions need footprints as well as types#

Local invalidation stops being local once you call a function through a mutable reference. If the callee may rewrite the whole packet, every relationship could be stale when it returns. Tether therefore needs a small notion of write footprint alongside ordinary function types.

fn markSeen(packet: &mut Packet)  writes { packet.lastSeen }{  packet.lastSeen = Clock.now()}

A call to markSeen preserves size without proving it again because the write set does not intersect either endpoint. A helper that receives only &mut packet.body would reopen links mentioning body for the duration of that borrow. A function that gets unrestricted mutable access has to return with the affected links closed.

There is an old idea hiding underneath this. Separation logic's frame rule is about local reasoning: a proof about the piece of state an operation touches can be carried out while unrelated state is framed around it. The details are different, but that instinct is exactly what I want here. The compiler should know that changing one corner of a value does not make every fact about the rest of it suspicious. Software Foundations has a readable treatment of the reasoning rules and frame rule.

Relationships should cross function boundaries#

Once links exist only inside records, programmers will immediately reinvent them in function comments. A split operation has relationships between its input and both outputs even though there is no record that owns all three values.

fn splitAt(bytes: Bytes, n: Nat)  -> (left: Bytes, right: Bytes)  ensures {    left.len + right.len == bytes.len    left.len == min(n, bytes.len)  }

Tether should put those postconditions into the caller's local relationship graph. The returned byte strings remain plain Bytes. The caller also learns that their lengths add back to the original length and that the left side has the requested capped length. Keep both values around and those facts are available to later checks. Drop one endpoint and the relationship can disappear with it.

This is where I would resist making every proof first-class by default. Most code wants to use the fact, not store a certificate object for it. The compiler can erase solver facts completely. An explicit witness value can exist as an escape hatch for generic proof-heavy code, but making every ordinary call traffic in witness terms would recreate the surface area I was trying to avoid.

This is not new logic#

A sufficiently expressive refinement type system can already state these predicates. Jhala and Vazou's refinement types tutorial is a good map of the territory: ordinary types are narrowed by logical predicates, with automation doing as much of the checking as is practical. Idris attacks the problem from a dependent-type direction, and its documentation even shows that dependent record fields can be updated together when they depend on each other.

Tether is a language-design opinion on top of that territory. It says the dependency graph itself deserves to be visible to the source language and compiler because mutation, diagnostics, and API boundaries all care about which values participate in a fact.

Indexed types remain better when the index is part of the algorithm. Matrix dimensions, protocol states, and vectors whose length controls recursion genuinely want that information in the type. I would not make a matrix library worse just to avoid writing Matrix<m, n>.

Tether is aimed at the less glamorous invariants that pile up in systems code: cached counts, source ranges, payload lengths, image buffers, offsets into mapped files, and values imported from foreign APIs. These facts are important, but callers often do not want them promoted into permanent type parameters.

Keep the solver aggressively boring#

A prototype should not begin by trying to prove arbitrary programs. Equality, ordering, integer ranges, and linear arithmetic already cover the examples that motivated the language. Library functions can expose trusted or separately checked postconditions such as take(xs, n).len <= n. Anything beyond the automatic fragment can require an explicit proof function.

Internally, I would lower each link to a predicate plus an endpoint set. SSA conversion gives each write a new value. A write invalidates the links that mention the old endpoint; assignments, branches, and function postconditions add facts; the end of an edit asks the solver to discharge the open obligations. Successful proof evidence is erased, so a Packet at runtime is still just a length and some bytes.

The first real program should be boring too#

I would not test this language with red-black trees or a theorem about addition. I would write a medium-sized binary parser and serializer, then an image buffer library. Those programs are full of values that are ordinary on their own and constrained only because a format or data structure placed them next to something else.

The useful measurement would not be “how many proofs did Tether verify?” It would be how often application code still has to repeat a check, how many public signatures acquire type-level plumbing, how far an invariant failure is reported from the write that caused it, and whether an ordinary edit feels ordinary.

The previous article's pitch was to put a type on the edge between two fields. The language version is a little stronger: make that edge something the compiler can preserve, invalidate, repair, and explain. If Tether is worth building, it will not be because link is cute syntax. It will be because local relationships can stay local even after the program starts changing things.