essay

Welcome to Brass Language

A programming language designed for AI to write and humans to trust

Today, AI models write code in programming languages that were never designed for AI. Languages like C++, Python, and Rust were designed for people who did that now-ancient thing of writing code by hand. Because these languages were designed for people, they were also designed with human-level productivity gains in mind, introducing all sorts of clever abstractions and dependencies — the kind of behavior that offers accelerated development when writing code by hand, but brings unnecessary effort and confusion to LLMs trying to reason out a large code base (AKA navigating 5 parent classes to understand one method).

That is why Brass exists: a programming language designed for AI to efficiently program with.

By being AI-first, Brass creates code that isolates context as much as possible and offers built-in code navigation tooling, offering concise situational awareness within a couple of files or commands rather than the traditional reason → grep → reason → grep-again AI loop. As a result, an AI model writing code in Brass has less to look up to build context, even if the model is unfamiliar with the language. And curiously enough, by stepping away from traditional coding patterns like inheritance, Brass gains an explicitness that is also easier for people to read and review than the sort of code language models commonly write today.

That explicitness is also what makes Brass checkable. Each module declares what its functions need, what they promise and which state changes they may make. Before the code can run, Brass’s checker has to prove that the code does what those declarations say. If it can’t, the code is rejected. What nothing checks is labeled assumed, so a reviewer can see what the program takes on faith.

Jumping into the language itself, the intention of this document is to introduce Brass and its key features. Think of it as a “getting to know you” guide for a new programming language. As part of this, it’s worth calling out that Brass is still a spec language; nothing compiles yet, so think of Brass as an exploration of an idea and a request for comment.

Today there is a grammar rule book for models to follow, and brass, a working tool that checks a program’s structure, runs its examples and helps models find their way around the code (see How a model uses the tool and The impact of this work). Next comes the full checker, which proves every function's promises, then a compiled runtime.

Let’s go exploring!

The basic idea – dinosaur enclosures

An alarm has tripped and a paddock’s door has been closed. The park’s record for that paddock now has to change from open to secured. Other systems read this record, so the change must be assigned to the correct paddock.

In bringing this logic to Brass, let’s first go over what a Brass module looks like. Each Brass module (file) is composed of up to three sections:

• interface holds the declarations that are publicly accessible to other modules.
• private holds declarations that can only be used by the internals of this file. This section is optional.
• body holds the implementations of the code defined in interface and private. Any changes to the body must match declarations outside the body.

The file below implements the paddock situation described above. Note that there is no private section and the public function secure takes an open paddock and returns a secured one with the same id.

# park/enclosures.brass, first version
module park.enclosures

interface
  # the states an enclosure can be in, and the moves allowed between them
  machine Enclosure
    states  Secured, Open, Breached
    initial Secured
    Secured enters Open
    Open    enters Secured | Breached

  type Paddock        = { id: Int where it in 1 to 40, status: Enclosure }
  type OpenPaddock    = Paddock where it.status in {Enclosure.Open}
  type SecuredPaddock = Paddock where it.status in {Enclosure.Secured}

  # a first version: it only updates the record
  # the code samples that follow build on it, up to closing the real door
  fn secure(p: OpenPaddock) -> SecuredPaddock
    after result.id == p.id

body
  # with copies p; enters changes its status, and only along a declared move
  fn secure(p) = p with { status enters Enclosure.Secured }

Each part of secure has one job:

• p: OpenPaddock accepts only a paddock whose record is open.
• -> SecuredPaddock requires the result to be a secured paddock.
• after result.id == p.id requires the result to have the same id as the paddock passed in. This promise stays in place and must be honored regardless of how the implementation of secure changes inside the body.
• Here the body implementation of secure is one line: a copy of p with its status changed to Enclosure.Secured by using the enters keyword, allowing the state to change in an explicit manner, and only along a move the machine declares. That one line is also the function’s result; Brass has no return keyword.

The function can only modify a configuration or subsystem if it is given access to that item as a parameter. secure’s only parameter is the paddock record, so it can return an updated copy of the record, but it cannot do some other arbitrary task like close the actual door unless given access to that behavior. This sort of code access/isolation is central to Brass’s approach towards explicitness.

Now suppose a model edits the body and leaves in a test value, so every result gets id 1.

-  fn secure(p) = p with { status enters Enclosure.Secured }
+  fn secure(p) = p with { id: 1, status enters Enclosure.Secured }

This edit produces the following error, since p.id is not always 1:

fault after not established: result.id == p.id
  counterexample: p.id = 2
  at park/enclosures.brass: fn secure
  fix: leave id as it is in p

The result has the right type, but the wrong id for every paddock except 1, breaking the declared promise after result.id == p.id and thus rejecting the code change via a fault.

State machines: declaring which state changes are allowed

The code above makes use of machine to create a state machine named Enclosure. In this context, Enclosure defines the following states and moves: a secured paddock can transition to open, and an open paddock can transition to secured or breached. Once a paddock becomes breached, it is locked in that state. Eventually, adding something like a repair move would allow breached to shift back to secured; that changes the machine, which is part of the interface, so it is a decision for a person.

brass and what it means when an edit is accepted

With the full checker, brass only accepts an edit once it has proven every promise the module makes. It doesn’t matter how the edit was made: whether a model went through brass apply or wrote the file directly, brass check reads the files as they are, and nothing runs until a check passes and brass writes its lock file. For enclosures.brass that is three facts:

• Any code that calls secure has to hand it a paddock that’s known to be open (an OpenPaddock).
• What secure returns is of type SecuredPaddock and has the same id.
• Every Enclosure state change must be a move the machine declares.

The checker proves only what the declarations say. If there is a rule that is missing, such as closing the physical door, this won’t be caught. See What it catches, and what it misses for more detail.

Writing down a promise

A promise is a contract that must prove true for a function to successfully enter or exit its execution. Promises allow critical “this must be true for the function to be useful” logic to be made explicit, allowing the function implementation to focus on business logic rather than the proof required to support this logic.

You write a promise with before or after. A third line, example, works like a built-in test: one call and the answer it must give.

So far the park has used only after; before and example arrive as it grows.

Together, the before and after lines are what the spec calls a contract. Once declared, the checker has to prove every contract holds, or it rejects the program, in turn naming the clause it couldn’t prove. For promises connected to outside software boundaries, see What it catches, and what it misses.

Where Brass departs from the usual form

Before moving to the next phase of code development, let’s spend a moment to consider the language in broader terms. Though most of Brass will look familiar, the differences you’ll notice come from three critical design choices:

1. Keep meaning local. Business logic is kept as local to the source file as possible. This means Brass leaves out inheritance, dynamic dispatch and mutable global state, to cut down on the cross-file detective work that generally comes with navigating a pre-AI language.
2. Say it one way. Each Brass keyword has one meaning, or a few closely related ones, and tries to narrow its use case to one kind. This means no overloading and no mixing of metaphors (such as using + to mean the summing of numbers and the concatenation of strings).
3. Put the rules beside the function. What a function needs, promises and may touch goes in its signature, so a model can read the rules associated with a function before it reads its implementation.

Together with the brass tooling, these choices mean a model can get what it needs from a module’s declarations in one or two commands instead of reading bodies across many files, and when an edit fails, the checker names the rule it broke.

Why it is built this way

In thinking about the design of Brass, it’s fair to think:

Writing code can mean building lots of things: a game, an operating system, a spreadsheet, the flow logic for a pacemaker… Though these things are the result of software producing a specific behavior, that behavior only exists because code segments were described in relationship with each other.

Code is about relationships. Or more specifically, code describes relationships between data to produce a result.

And in today’s world, relationships are complex. Major commercial software easily runs to tens of millions of lines of code (a bad unit of measurement I know, but bear with me), and that number only grows. As a codebase grows, so do the relationships within it, and keeping track of them gets expensive.

Brass accepts that keeping those relationships correct has a cost, and leans into it with two rules:

• Records repeat shared fields. A record is a type with named fields, like Paddock. Each one lists all its own fields, even ones another record shares, so what a model needs is in one place. The bet is that this costs less than untangling deep inheritance.
• The checker rejects code it cannot prove. It names the clause it couldn’t prove, as the id 1 edit showed, and never guesses what you meant or relaxes a promise to let code through. Sometimes that rejects correct code, and the model tries again. Letting a broken promise through would cost a door left open.

None of these ideas is new on its own. Cargo locks dependencies, E passes authority around as a value, and Dafny proves contracts before code runs. Yes, Brass borrows from a bunch of languages, and it could easily turn into a Dagwood of a language. So every borrowed idea has to pass one simple test: can you tell what a module needs, does and promises just by reading its declarations? If yes, it’s in. If not, it’s out.

Dinosaurs continued – building out the park

Continuing with the dinosaur park, let’s add more detail to the paddock records, introduce a module that controls the doors, and handle things going wrong. To help tell what’s new from what’s existing, new lines appear in blue, removed lines are shown in strikethrough, and unchanged code is colored gray.

Types and examples

For this code let’s do a few things: give Paddock its own typed ID via PaddockId, add a species to each paddock, and create the scaffolding for staff records. As you’ll see in the code, by using where, a type can carry an extra condition, such as a PaddockId within a specific integer range, or a DoorOperator described as a staff member whose role is Operator.

# park/enclosures.brass
 interface
+  type PaddockId = Int where it in 1 to 40
+  type BadgeId   = Int where it in 1 to 9999
+  type Grams     = Int where it in 0 to 50000
+  # a sum type: one of these names, written Species.Rex elsewhere
+  type Species   = Goat | Raptor | Rex      # the goats are lunch
+  type Role      = Keeper | Operator | Guide
+  type Staff        = { badge: BadgeId, role: Role }
+  type DoorOperator = Staff where it.role in {Role.Operator}

   machine Enclosure   # unchanged

-  type Paddock        = { id: Int where it in 1 to 40, status: Enclosure }
+  type Paddock        = { id: PaddockId, species: Species, status: Enclosure }
   type OpenPaddock    = Paddock where it.status in {Enclosure.Open}
   type SecuredPaddock = Paddock where it.status in {Enclosure.Secured}

   fn secure(p: OpenPaddock) -> SecuredPaddock
-    after result.id == p.id
+    after result.id == p.id and result.species == p.species
+
+  # an example: one call and its answer, run on every check
+  fn ration(species: Species) -> Grams
+    example ration(Species.Goat) == 2000
+    example ration(Species.Rex) == 50000

 body
   fn secure(p) = p with { status enters Enclosure.Secured }
+  fn ration(species) =
+    if species in {Species.Goat} then 2000
+    else if species in {Species.Raptor} then 12000
+    else 50000

Two things about this code are worth pointing out before moving on.

• A value gets a where type only when the checker can prove it fits, or an is test succeeds. Once who is DoorOperator passes, Brass treats who as a DoorOperator for the rest of that branch. Brass has no casts.
• Examples and proofs work together. ration’s two example lines run on every check; separately, the checker proves every answer fits in Grams. Examples are only for functions that can’t fail and take no access.

Authority is a parameter

So far, secure only changes a record. To actually close a door, Brass must call the host (Brass’s name for the outside software it talks to). Here that is the park’s existing control-room software, which reads sensors, runs the door motors, and keeps records. A function reaches the host only through an access: a parameter that lists which host operations it may call. Every call through an access is a request to software outside Brass; the host does the work and sends back a reply. Here the access is Doors, with two operations: look up a paddock and close its door.

When a motion sensor trips, the host calls lockdown_request with the person at the console and the paddock number. A function the host can call is an entry point. Its access comes from a grant in system.brass, which also limits which doors it covers. The function checks the person’s role, asks the host to close the door, and returns the secured paddock or an error. The host records that result (the log.record line below), and the rest of the park reads it.

# the control room's side, sketched in Python; the call shape is illustrative
who    = db.staff(console.badge)
# doors is not passed: the runtime fills it from the grant in system.brass
result = brass.call("park.doors.lockdown_request", who=who, paddock=alarm.paddock)
log.record(result)   # an Ok with the secured paddock, or an Err with a code and a message

# park/doors.brass
module park.doors
import park.enclosures as enclosures

interface
  # what the host provides; each allow is one operation the host implements
  access Doors { paddocks: Set<enclosures.PaddockId>, deadline_ms: Int }
    allow enclosure(paddock: enclosures.PaddockId) -> Outcome<enclosures.Paddock>
      before paddock in paddocks
      after  result.id == paddock
    allow close(operator: enclosures.DoorOperator, paddock: enclosures.PaddockId) -> Outcome<Done>
      before paddock in paddocks

  # the entry point: the host calls it with plain staff and a paddock number; the role is tested inside
  fn lockdown_request(doors: Doors, who: enclosures.Staff, paddock: enclosures.PaddockId) -> Outcome<enclosures.SecuredPaddock>
    after result.id == paddock

# only this file can use what private declares
private
  fn lockdown_as(doors: Doors, operator: enclosures.DoorOperator, paddock: enclosures.PaddockId) -> Outcome<enclosures.SecuredPaddock>
    after result.id == paddock

body
  fn lockdown_request(doors, who, paddock) =
    if who is enclosures.DoorOperator then lockdown_as(doors, who, paddock)
    else Err(FailureCode.Unauthorized, "not a door operator")

  fn lockdown_as(doors, operator, paddock) =
    let p: enclosures.Paddock = doors.enclosure(paddock)?
    if p is enclosures.OpenPaddock then
      doors.close(operator, p.id)?
      Ok(enclosures.secure(p))
    else Err(FailureCode.Conflict, "paddock is not open")

# system.brass: the one file that creates authority
system park
  grants park.doors.lockdown_request: doors = Doors { paddocks: {1, 2, 3}, deadline_ms: 30000 }
  # and three required limits and an optional review policy, shown in the complete program

• access lists the host operations available to the code. Within it, each allow declares one operation. doors.close(…) looks like a method call, but doors is an access, and close is one of the operations it allows. The runtime checks both sides of every call: the before going in, the after coming back. Here, access covers paddocks 1 to 3, and deadline_ms allows each operation 30 seconds to reply, enough time for a heavy gate to close.
• Access is passed through parameters. The runtime supplies doors from the grant: the line in system.brass that names an entry point and hands it an access with specific bounds. No grant, no access. lockdown_request then passes doors to lockdown_as, which calls its operations. Access cannot be stored or returned. secure receives none.
• close requires a DoorOperator. Having doors is not enough: the staff member must also have the required role.

Below are four possible host calls and their results, written in the host’s notation. The error messages are illustrative.

lockdown_request(who: operator, paddock: 2)
  → Ok({ id: 2, species: Raptor, status: Secured })

lockdown_request(who: guide, paddock: 2)
  → Err(FailureCode.Unauthorized, "not a door operator")           # the body's own refusal

lockdown_request(who: operator, paddock: 7)
  → Err(FailureCode.Unauthorized, "paddock in paddocks")           # the authority check on enclosure refused; the grant covers 1 to 3

lockdown_request(who: operator, paddock: 41)
  → Err(FailureCode.InvalidInput, "paddock: enclosures.PaddockId")  # refused on the way in: 41 is not a PaddockId, and the body never ran

Failure is a value

lockdown_as has three places where it can return an error: reading the paddock, closing the door, and finding that the paddock isn't open. All three come back the same way, as an error value in the return type rather than an exception. Every error carries one of Brass’s standard failure codes, the closed list below, plus a message. A body picks the code that fits; it can’t invent new ones.

# built in
type Outcome<T>  = Ok(T) | Err(FailureCode, Text)
type FailureCode = Unauthorized | InvalidInput | Conflict | Unavailable | ResourceExhausted | Other | Unknown | NotFound

# park/doors.brass
 private
   fn lockdown_as(…) -> Outcome<enclosures.SecuredPaddock>
     after result.id == paddock
 body
   fn lockdown_as(doors, operator, paddock) =
+    # ? gives the Ok value, or leaves the function now, handing the Err to its caller
     let p: enclosures.Paddock = doors.enclosure(paddock)?
     if p is enclosures.OpenPaddock then
       doors.close(operator, p.id)?
+      # the last line of a branch is its value
       Ok(enclosures.secure(p))
+    # every failure (Err) carries a code and a message
     else Err(FailureCode.Conflict, "paddock is not open")

• after describes success only. lockdown_as promises after result.id == paddock. On a function that returns an Outcome<T>, that promise is about the value inside Ok: when the function succeeds, the paddock it returns has the id it was asked for. When it returns an Err, there is no result to promise anything about.
• Brass has no exceptions. ? unwraps the value inside Ok so the next line can use it. If the call came back as an Err instead, the function stops right there and hands that Err back to whoever called it. ? works only in functions that return an Outcome. To handle the result directly, use is Ok or is Err.
• Errors do not undo earlier actions. If the door closes and a later step fails, the door stays closed. Brass has no notion of a set of actions that succeed or fail together. A few failures aren’t errors at all and stop the whole call; see When a call stops.

How a model uses the tool — AKA less grep to build context faster

brass lets a model ask questions about unfamiliar code without reading every file. The session below shows the workflow: read the modules’ declarations, ask about one declaration, edit the code, and check the result.

In other words, brass stops the model from leaning on grep and gives it the semantic information it needs to build context.

Let’s consider a scenario where the model is asked to let the control room secure a paddock in any state. Every command below is part of brass today, and the models in the trials used each one. Every line that reports a proof, proven, rejected and ✓ every contract proven, shows the full checker at work: what brass reports once it proves promises and state moves.

$ brass show enclosures doors
file  park/enclosures.brass   declarations, lines 1 to 28 of 36
module park.enclosures

interface
  type PaddockId = Int where it in 1 to 40
…
  type Paddock        = { id: PaddockId, species: Species, status: Enclosure }
…
  fn secure(p: OpenPaddock) -> SecuredPaddock
    after result.id == p.id and result.species == p.species
…
file  park/doors.brass   declarations, lines 1 to 18 of 30
…
  fn lockdown_request(doors: Doors, who: enclosures.Staff, paddock: enclosures.PaddockId) -> Outcome<enclosures.SecuredPaddock>
    after result.id == paddock

private
  fn lockdown_as(doors: Doors, operator: enclosures.DoorOperator, paddock: enclosures.PaddockId) -> Outcome<enclosures.SecuredPaddock>
    after result.id == paddock

$ brass info park.enclosures.secure
info park.enclosures.secure  q:81c0d2e9a7f4
  fn secure(p: OpenPaddock) -> SecuredPaddock      proven
    after result.id == p.id and result.species == p.species      proven
  holds     no access; cannot reach outside
  used_by   1 declaration, 1 line
    doors.brass:29   Ok(enclosures.secure(p))
      in       fn lockdown_as(…) -> Outcome<enclosures.SecuredPaddock> (private)
      on path  if p is enclosures.OpenPaddock then
  body      1 line   references: Enclosure.Secured
end q:81c0d2e9a7f4

$ brass apply <<'PATCH'
@@@ edit park/enclosures.brass
@@@ find
  fn secure(p: OpenPaddock) -> SecuredPaddock
@@@ replace
  fn secure(p: Paddock) -> SecuredPaddock
@@@ end
PATCH
apply       ✗ nothing written: the check rejects 1 line
rejected    in the patched files:
  fault edge not established: p.status enters Enclosure.Secured
    source states not covered: Secured, Breached
    at park/enclosures.brass: fn secure
    fix: narrow p to a state with that edge, or test p is OpenPaddock first
held        1 block that matched, kept for your next apply

$ brass apply --drop
apply       held patch discarded

$ brass check
check       ✓ every contract proven or enforced, every edge established
grants      ✓ Doors { paddocks: {1, 2, 3}, deadline_ms: 30000 } fits park.doors.Doors
examples    ✓ 2 found, 2 hold
lock        written

All four commands work today.

What it catches, and what it misses

The checker can enforce what’s declared, but it cannot tell whether you’ve declared everything that matters. No compiler or type checker in any language can; a missing rule looks the same as a rule you chose not to write. Below are three edits a model might confidently make, and how far the checker’s protection goes on each.

# park/enclosures.brass
interface  fn ration(species: Species) -> Grams    example ration(Species.Goat) == 2000    example ration(Species.Rex) == 50000body  fn ration(species) =    if species in {Species.Goat} then 2000    else if species in {Species.Raptor} then 12000    else 50000    else 20000

$ brass check
examples    ✗ 2 found, 1 holds, 1 fails
  FAILS    enclosures.ration   park/enclosures.brass:28
           ration(Species.Rex) == 50000   got 20000

# park/doors.brass
body  fn lockdown_as(doors, operator, paddock) =    let p: enclosures.Paddock = doors.enclosure(paddock)?    if p is enclosures.OpenPaddock then      doors.close(operator, p.id)?      Ok(enclosures.secure(p))    else Err(FailureCode.Conflict, "paddock is not open")    doors.close(operator, p.id)?    Ok(enclosures.secure(p))

$ brass check
fault argument type: expected enclosures.OpenPaddock, found enclosures.Paddock
  at park/doors.brass: fn lockdown_as, enclosures.secure(p)
  fix: test p is enclosures.OpenPaddock first, or pass an OpenPaddock

# park/doors.brass
private  fn lockdown_as(…) -> Outcome<enclosures.SecuredPaddock>    after result.id == paddockbody  fn lockdown_as(doors, operator, paddock) =    let p: enclosures.Paddock = doors.enclosure(paddock)?    if p is enclosures.OpenPaddock then      doors.close(operator, p.id)?      Ok(enclosures.secure(p))    else Err(FailureCode.Conflict, "paddock is not open")

$ brass check
no rejection: every before and after still holds

The record says Secured. The door is still open.

The third edit shows the limit of what contracts say: a before covers the inputs and an after covers a successful result, and neither says what the body does in between. Which operations a body calls, how many times and in what order, is left to a reader or a test.

Caution Past this point, the checker only knows what the host tells it.

There is a second limit, and it has nothing to do with what the code says. Even when the code does ask the host to close the door, the host could report the door as closed when it isn't. Brass has no way to see that, which is why the report on lockdown_request lists it as assumed:

$ brass info park.doors.lockdown_request
info park.doors.lockdown_request  q:3f2a9c81e0d4
  fn lockdown_request(doors: Doors, who: enclosures.Staff, paddock: enclosures.PaddockId) -> Outcome<enclosures.SecuredPaddock>   enforced
    after result.id == paddock              enforced      # rests on enclosure's after, which the runtime checks
  holds     doors: Doors { paddocks: {1, 2, 3}, deadline_ms: 30000 }
  boundary  who: enclosures.Staff, paddock: enclosures.PaddockId   checked on entry   enforced
            who's identity, and that the paddock is really open                assumed
            that a door is shut when close returns Ok                          assumed
  used_by   none; granted entry point
end q:3f2a9c81e0d4

The word at the end of each row is the label brass puts on every promise. It says what supports the promise:

• proven: the checker proved it before the program runs.
• enforced: the runtime checks it on every call, as it does with the paddock number coming in and the host’s reply.
• assumed: nothing checks it. The program goes forward as if it held, and the label shows the reviewer exactly what they are taking on faith.

Put another way, Brass is good at expressing rules in code; the quality of those rules is up to whoever writes them.

The impact of this work

A model needs context to change code successfully. Normally, gathering this context means a lot of back-and-forth: read a file, follow a reference, run a check. Brass’s grammar and tooling bring more of that information into each response, reducing the back-and-forth.

To measure this, Claude Sonnet added a feature to the same expense-report program in Brass and in Python, across 40 sessions and three scenarios. Here, Brass means the language plus its tooling: the brass command, a project map and a host contract, a short list of the operations the outside software provides. Python had ordinary file tools only. Brass with file tools alone, and the full numbers, are in The AI Token Efficiency of Brass.

With Brass, the model made fewer than half as many requests and used less than half the context it did with Python.

Total context adds up everything sent to the model on every request, so text sent again on a later request is counted again. Each end of a range is one scenario’s average over five sessions. The AI Token Efficiency of Brass covers what the runs cost.

When getting to know the code base, the model gathered context in fewer requests with Brass, but with Python the model spent fewer tokens reasoning out the solution: in every scenario the Brass sessions thought 1.4 to 1.8 times as much. That makes sense, since the model has seen a vast amount of Python and none of Brass, though that cause hasn’t been measured. And two of the fifteen Brass sessions missed at least one test case, where every Python session passed. A few other findings matter:

• Brass’s context grew faster on a codebase 2.5 times larger. It rose 75% against Python’s 46%, but stayed under half of Python’s.
• The tooling helps Python too. Brass sessions start with a map of the project’s modules. In an earlier test, giving Python a comparable tool and map removed about three quarters of the difference in total context on the larger codebase. Brass still used the least. That’s worth exploring further, since the same idea could cut token use in languages people already use.
• Settling a design question cut reasoning. In an earlier trial, the model spent extra effort on a field that had to hold the state of one of two different state machines; in park terms, a field that could hold either a paddock’s state or a feeding schedule’s state. The language hadn’t said how to type such a field, so the confusion was in Brass, not in the task. The rule was settled (one shared list of step names, with a converter from each machine) and the trial rerun. Reasoning fell by nearly a third, and every session passed every test.

These runs cover one model, one program and two tasks. Brass is new, with no body of code for models to learn from. Further savings in both context and reasoning are expected, but not yet measured, as the language matures.

# park/enclosures.brass
module park.enclosures

interface
  type PaddockId = Int where it in 1 to 40
  type BadgeId   = Int where it in 1 to 9999
  type Grams     = Int where it in 0 to 50000
  type Species   = Goat | Raptor | Rex
  type Role      = Keeper | Operator | Guide

  type Staff        = { badge: BadgeId, role: Role }
  type DoorOperator = Staff where it.role in {Role.Operator}

  machine Enclosure
    states  Secured, Open, Breached
    initial Secured
    Secured enters Open
    Open    enters Secured | Breached

  type Paddock        = { id: PaddockId, species: Species, status: Enclosure }
  type OpenPaddock    = Paddock where it.status in {Enclosure.Open}
  type SecuredPaddock = Paddock where it.status in {Enclosure.Secured}

  fn secure(p: OpenPaddock) -> SecuredPaddock
    after result.id == p.id and result.species == p.species
  fn ration(species: Species) -> Grams
    example ration(Species.Goat) == 2000
    example ration(Species.Rex) == 50000

body
  fn secure(p) = p with { status enters Enclosure.Secured }

  fn ration(species) =
    if species in {Species.Goat} then 2000
    else if species in {Species.Raptor} then 12000
    else 50000

# park/doors.brass
module park.doors
import park.enclosures as enclosures

interface
  access Doors { paddocks: Set<enclosures.PaddockId>, deadline_ms: Int }
    allow enclosure(paddock: enclosures.PaddockId) -> Outcome<enclosures.Paddock>
      before paddock in paddocks
      after  result.id == paddock
    allow close(operator: enclosures.DoorOperator, paddock: enclosures.PaddockId) -> Outcome<Done>
      before paddock in paddocks

  fn lockdown_request(doors: Doors, who: enclosures.Staff, paddock: enclosures.PaddockId) -> Outcome<enclosures.SecuredPaddock>
    after result.id == paddock

private
  fn lockdown_as(doors: Doors, operator: enclosures.DoorOperator, paddock: enclosures.PaddockId) -> Outcome<enclosures.SecuredPaddock>
    after result.id == paddock

body
  fn lockdown_request(doors, who, paddock) =
    if who is enclosures.DoorOperator then lockdown_as(doors, who, paddock)
    else Err(FailureCode.Unauthorized, "not a door operator")

  fn lockdown_as(doors, operator, paddock) =
    let p: enclosures.Paddock = doors.enclosure(paddock)?
    if p is enclosures.OpenPaddock then
      doors.close(operator, p.id)?
      Ok(enclosures.secure(p))
    else Err(FailureCode.Conflict, "paddock is not open")

# system.brass
system park
  grants park.doors.lockdown_request: doors = Doors { paddocks: {1, 2, 3}, deadline_ms: 30000 }
  limit  cpu_ms 5000
  limit  memory_bytes 268435456
  limit  transcript_bytes 67108864, drop oldest
  limit  impact_modules 4

# park/doors.brass: lockdown_as with a bounded retry
fn lockdown_as(doors, operator, paddock) =
  let p: enclosures.Paddock = doors.enclosure(paddock)?
  if p is enclosures.OpenPaddock then
    # every let is typed
    let last: Outcome<Done> = Err(FailureCode.Unavailable, "not tried")
    # bounded by its range: 1, 2, 3
    for attempt in 1 to 3
      # a rebinding of the same type, not a mutation
      last = doors.close(operator, p.id)
      if last is Ok then break
    if last is Ok then Ok(enclosures.secure(p))
    else Err(FailureCode.Unavailable, "door did not close in three attempts")
  else Err(FailureCode.Conflict, "paddock is not open")

# park/enclosures.brass
fn open_ones(ps: Array<Paddock> where it.length in 0 to 40) -> Array<OpenPaddock> where it.length in 0 to 40
fn open_ones(ps) =
  let found: Array<OpenPaddock> = []
  for p in ps
    if p is OpenPaddock then found = found ++ [p]
  found

# park/enclosures.brass
fn predator_loose(ps: Array<Paddock> where it.length in 0 to 40) -> Bool
fn predator_loose(ps) = any p in ps where p is OpenPaddock and p.species in {Species.Raptor, Species.Rex}

# park/enclosures.brass
fn signers(first: BadgeId, second: Maybe<BadgeId>) -> Int
fn signers(first, second) =
  # on the right of and, second counts as a plain BadgeId
  if second != None and second != first then 2 else 1

# park/doors.brass, inside lockdown_as
doors.close(@@operator, p.id)?