Verse’s Theoretical Roots: The Verse Calculus

1. A Language With a Paper for Armor

Most game scripting languages are born “make it run first, document it later”. Verse went the other way: it’s a deterministic functional logic language, and its core calculus, The Verse Calculus, was published as a paper at ICFP 2023, a top-tier venue in programming language research. The author lineup is stacked: Lennart Augustsson (author of one of the earliest Haskell compilers), Simon Peyton Jones (one of Haskell’s fathers and the soul of GHC), and Tim Sweeney (founder of Epic Games), among others, joined forces. Getting the people who wrote Haskell to design a game scripting language — that’s roughly what “gloriously over-provisioned” looks like in language design.

The “functional logic language” school kneads two styles together: one is functional — everything is “computing a value”, and once computed you don’t go around mutating data everywhere; the other is logic-style — you only describe “what counts as a valid solution”, and the actual work of finding it is handed to the language itself. And “deterministic” is a rule Verse set for itself: the same input always gives the same result — it won’t toss you a “whatever fate decides” answer the way some logic languages do. Those designs in Lesson 12 that looked so eccentric — if testing success, failure that rolls back, no error-and-crash routine — every one of them has a rigorous mathematical definition in this paper.

2. Zero Values, One Value, Many Values

The paper’s core insight fits in one sentence: treat “failure” and “choice” as the language’s headline concerns. In the traditional way of thinking, you compute something and, as a matter of course, get one value back; in Verse’s model, computing something can yield zero, one, or even several values:

# Semantics sketch (you can't write these bare: failable expressions must live in a failure context)
# One value: the comparison holds, the expression succeeds
3 < 5

# Zero values: the comparison doesn't hold, the expression "fails" - not false, but no value at all
5 < 3

# The true face of if: at least one value from the condition takes then, zero values takes else
if (X := Items[0]):
    Print("Got {X}")
else:
    Print("Zero values produced this time")

The precise definition of “failure” in this account is exactly: the computation produced zero values. So Verse’s if needs no boolean whatsoever — it just counts how many values the condition produced: at least one, take then (stashing that value for you to use on the way); none at all, take else. “Many values” corresponds to “choice”: one computation can lay out several candidate values, and the reason for / ForEach can take values one at a time is built precisely on this — which is also why in Lesson 14 you’ll see for collect each round’s result into an array. if and for aren’t two separate things; they’re two faces of the same “how values are produced, how values are collected” story.

The paper also fits this semantics with a set of “step-by-step equivalent rewriting” reasoning rules (called small-step rewrite semantics): whether two programs are truly equivalent goes from “gut feeling” to something you can strictly prove. That puts a safety line under engine optimizations (including the lenient evaluation from Lesson 12’s extra page): as long as a rewrite is proven equivalent before and after, the engine can confidently rearrange your logic.

3. What This Means for You, Writing Device Code

You don’t have to read the Greek letters in the paper to write good Verse, but knowing the bedrock is there brings three very real benefits. First, the story is unified: if conditions, for / ForEach filters, lifting a value out of an option with ?, calling failable functions with square brackets — they’re all different outfits for the same single thing, “producing zero or several values”; learn one and you’ve learned the whole family. Second, rollback is trustworthy: speculative execution (that “shadow graph”) and effect rollback are rigorously defined at the calculus level, not patched in after the fact, so you can confidently put “tentative changes” inside a failure context. Third, the restrictions make sense: banning return, and banning world-changing actions inside conditions, both defend the cornerstone of “can two programs be reasoned about with an equals sign” — when the compiler stops you, it isn’t hazing; it’s standing guard for the mathematical model.

In other words: when you type if (Player := player[Agent]): in UEFN, thirty years of functional programming research is standing behind that line. For a game scripting language, that’s a luxuriously deep bench.

4. Sources and Further Reading

This page is compiled from material published by the paper’s authors. Want to leaf through the original yourself (English; Greek letters ahead)? These entrances, sorted by friendliness:

▸ The Verse Calculus project page (Simon Peyton Jones’s homepage) ↗

▸ Paper PDF: The Verse Calculus — a core calculus for deterministic functional logic programming ↗

▸ ACM Digital Library entry (ICFP 2023) ↗

Not finishing the paper won’t hold you back one bit in this handbook — but the next time someone asks you “why is Verse’s if so weird”, you can reply, perfectly composed: “That’s not weird. That’s deterministic functional logic programming.”