The Fortress Language Specification, Version 1.0 α (Sun Microsystems, September 19, 2006; 411 pages) is the most deliberate attempt at mathematical notation in a general-purpose language. Its authors are Eric Allen, David Chase, Joe Hallett, Victor Luchangco, Jan-Willem Maessen, Sukyoung Ryu, Guy L. Steele Jr. and Sam Tobin-Hochstadt, who gives the State of Racket on Sunday.

Four ideas from the spec, quoted from sections 2.4, 2.12, 2.13 and 16.7:

Rendering

programs are typed in ASCII and displayed as mathematics. f(x) = x^2 + sin x - cos 2 x renders with a superscript and italics; a[i] renders as a subscript. Unicode can be typed by name: GREEK_CAPITAL_LETTER_LAMBDA becomes Λ, lambda becomes λ, SUM becomes Σ, CUP becomes ∪.

Comprehensions

set-builder notation, computed in parallel by default: {x/2 | x ← t}, {x + y | x ← s, y ← t}, {x | x ← t, x ≥ 0}.

Big operators

factorial(n) = PRODUCT[i <- 1:n] i, rendered as a capital pi over i ← 1:n.

Juxtaposition

2 x is multiplication and sin x is application. Which one depends on types and whitespace, so the parser holds a run of juxtaposed terms "in abeyance", type-checks each element, and only then rewrites it into a tree. The spec gives the case it forbids: if n is both a functional method and a local, na is a static error.

That last rule is the cost of mathematical notation stated plainly: the grammar cannot be parsed without the types.

Quoted from chapter 2 of the spec. The text was extracted from the PDF, which loses the rendering, so superscripts are restored here by hand and the blackboard-bold types are written as ℝ and ℤ.

Juxtaposition is multiplication, and a function next to its argument is a call (section 2.6):

factorial(n) =
    if n = 0 then 1
    else n factorial(n − 1) end

sin x

Comparisons chain as on paper, and parameters take defaults by keyword (2.6.1):

makeColor(red: ℤ64 = 0, green: ℤ64 = 0, blue: ℤ64 = 0) =
    if 0 ≤ red ≤ 255 ∧ 0 ≤ green ≤ 255 ∧ 0 ≤ blue ≤ 255
    then Color(red, green, blue)
    else throw Error end

makeColor(green = 255)

Contracts sit in the function header, before the body; result is bound in ensures (2.6.4):

factorial(n)
    requires n ≥ 0
    ensures result ≥ 0
    = if n = 0 then 1
      else n factorial(n − 1) end

Loops are parallel unless asked otherwise, so this may print in any order (2.8), and atomic is how parallel code shares state (2.9):

for i ← 1:10 do
    print(i " ")
end
-- possible output: 5 4 6 3 7 2 9 10 1 8

atomic do
    x += 1
    y += 1
end

Units and dimensions are part of the type, checked statically (2.10):

kineticEnergy(m: ℝ kg, v: ℝ m/s): ℝ kg m²/s² = (m v²)/2

v: ℝ m/s = (3 meters + 4 meters)/5 seconds    -- fine
v: ℝ m/s = (3 meters + 4 seconds)/5 seconds   -- static error: meters + seconds
v: ℝ m/s = (3 meters + 4 meters)/5            -- static error: m is not m/s

kineticEnergy(3.14 kg, 32 f/s in m/s)         -- unit conversion

Tests range over a finite collection; properties quantify over a type (2.14):

test factorialResultLarger[x ← 0:100] = x ≤ factorial(x)
property factorialResultAlwaysLarger = ∀(x: ℤ) (x ≤ factorial(x))

Where each idea went afterwards:

The "where it lives now" column is from memory, except that Treason depends on rackcheck, which its info.rkt shows.

Sam Tobin-Hochstadt is on the spec's author list, gives the State of Racket on Sunday, and works on Typed Racket. A question in the keynote that brought up Fortress would have had one of its authors in the room. Fortress's two hardest problems, type-directed parsing and parallel-by-default evaluation, are the two Racket never took on; its contracts and its typed treatment of an untyped notation are both things Racket did take on.

Haskell kept most of it without the type-directed parsing: comprehensions are set-builder notation, and operators can be Unicode with declared fixity, so ∩ binds tighter than ∪ as it does on paper. Run on GHC 9.14.1:

{-# LANGUAGE UnicodeSyntax #-}
import Data.List (union, intersect)

infixl 6 ∪
infixl 7 ∩
(∪), (∩) :: Eq a => [a] -> [a] -> [a]
(∪) = union
(∩) = intersect

infix 4 ∈
(∈) :: Eq a => a -> [a] -> Bool
(∈) = elem

halves t        = [x / 2 | x <- t]               -- {x/2 | x ← t}
sums s t        = [x + y | x <- s, y <- t]       -- {x + y | x ← s, y ← t}
nonNegative t   = [x | x <- t, x >= 0]           -- {x | x ← t, x ≥ 0}
factorial n     = product [i | i <- [1 .. n]]    -- PRODUCT[i <- 1:n] i

-- halves [2, 4, 6]                 => [1.0,2.0,3.0]
-- sums [1, 2] [10, 20]             => [11,21,12,22]
-- nonNegative [-1, 0, 3]           => [0,3]
-- factorial 10                     => 3628800
-- [1, 2, 3] ∪ [3, 4] ∩ [4, 5]      => [1,2,3,4]   (∩ first)
-- 3 ∈ [1, 2, 3] ∪ [4]              => True

What Haskell gave up is juxtaposition as multiplication: 2 x is application of 2. That single choice is what lets it parse without types.

Racket keeps prefix notation and puts the same ideas in named forms. Run on Racket 8.15:

(for/list ([x (list 2 4 6)]) (/ x 2))                ; => (1 2 3)
(for*/list ([x (list 1 2)] [y (list 10 20)]) (+ x y)) ; => (11 21 12 22)
(for/product ([i (in-range 1 11)]) i)                ; => 3628800, Π
(for/sum ([i (in-range 1 11)]) (* i i))              ; => 385, Σ

Rhombus is where Racket's answer moved: infix operators with declared precedence over the same macro system, and the enforestation step that Pille reuses on Saturday afternoon.

Questions to bring to the keynote: does notation belong in the language, in the renderer, or in the editor? Fortress put it in all three. Tableau, which Hanrahan co-founded, put it in the interface and kept the user away from syntax altogether.

Emeritus professor at Stanford (profile). The program has no abstract, and no earlier talk with this title turned up.

His language papers

the RenderMan shading language (SIGGRAPH 1990); Brook for GPUs (2004); Polaris (TVCG 2002), the visualization specification language that led to Tableau's VizQL; Terra (PLDI 2013).

Related talks

shading languages (SFU 2023); Hardware as Software (Lambda Days 2021); an NSF lecture transcript arguing for DSLs with precise semantics.

Probable background

Iverson, Notation as a Tool of Thought (1979 Turing Lecture).

GitHub capfredf; 144 commits in Typed Racket. The inference prototype has no public repository.

His papers, as Yuquan Fu (Indiana, with Tobin-Hochstadt)

Type Checking Extracted Methods (‹Programming› 2022); Revisiting Soundness for Occurrence Typing, Semantically (arXiv, September 2026, with Carlo Angiuli), which finds flaws in earlier soundness proofs for occurrence typing and replaces them with a step-indexed logical-relations proof mechanized in Lean.

Same person?

no page says Fred Fu and Yuquan Fu are one person. The evidence is a 2020 capfredf commit on the 2022 paper's topic.

Prior work

the title extends Logical Types for Untyped Languages (ICFP 2010). Algebraic subtyping: MLsub (POPL 2017, code), Dolan's thesis, and Simple-sub (ICFP 2020, code). Castagna et al., Revisiting Occurrence Typing, which formulates occurrence typing with semantic subtyping.

GitHub distractedlambda. distractedlambda/pille holds four Racket packages: the implementation, Rhombus bindings to the LLVM C API (including the ORC JIT), SPMD "varying" types, and the docs and tests. Last commit 2026-10-02. The Rhombus v1.0 announcement lists Pille as a language built on Rhombus.

Prior work

Rhombus (OOPSLA 2023); Honu (GPCE 2012), which introduced enforestation; Terra, an LLVM-compiled low-level language staged from Lua, co-authored by Hanrahan; the enforest docs.

GitHub quasarbright; blog; 184 commits in syntax-spec. Built and run in Step 2 below.

Prior work

syntax-spec (ICFP 2024); Fortifying Macros (ICFP 2010); Lean 4's Beyond Notations.

Compared against in the talk

racket-langserver and rust-analyzer.

University of Utah, on sabbatical at NVIDIA (homepage).

Code

herbie-fp/herbie (site), a Racket core with a Rust e-graph component; Rival for interval arithmetic; Odyssey, an interactive interface; FPBench, the benchmark suite.

Papers

Herbie (PLDI 2015); egg (POPL 2021); Combining Precision Tuning and Rewriting (ARITH 2021); Rival (ARITH 2023); equality saturation (POPL 2009).

Talks

PLDI 2015; NSV 2020.

Codeberg apropos; site toki.la. apropos/cio implements effect handlers for Racket and Guile on prompts; its core forms are define-effect, raise-effect, try, resume and with-effect-handler, and the README names Effekt as the main model. A second repository, racket-guile-control, reimplements Guile's delimited-control primitives in Racket.

Prior work

Effekt and Effects as Capabilities; Plotkin and Pretnar, Handling Algebraic Effects; Racket delimited control (ICFP 2007); Guile prompts.

Other Racket effect libraries

effect-racket, effection.

Czech Technical University in Prague (profile).

Code and docs

rmculpepper/racket-brandx; the docs cover interfaces, generics, bundles, signatures and dependent contracts; the August 2026 announcement gives the motivation. He is testing it by porting his crypto library.

Prior work

his own Fortifying Macros and Debugging Hygienic Macros; racket/generic; Classes, Mixins, and Traits (APLAS 2006); Contracts for First-Class Classes; Units, the model for BrandX's bundles and signatures.

Earlier talk

Making low-level libraries Rackety (RacketCon 2011 slides).

GitHub samdphillips. samdphillips/uke (docs) has dataframe, column, index and store layers; select, group and left-join return new values instead of mutating.

Comparable Racket libraries

data-frame, sawzall, tabular-asa.

Background

Towards Scalable Dataframe Systems (VLDB 2020).

University of Utah (homepage).

Code and docs

the ffi2 docs; the package ffi2-lib, whose source is in racket/racket starting at commit 6927f16 (authored 2026-03-13). Two earlier commits change Chez Scheme: one adds __errno and __alloc foreign conventions, one adds nongenerative define-ftype. The v9.2 notes mention ffi2; Rhombus's ffi library is built on it.

Prior work

Barzilay and Orlovsky, Foreign Interface for PLT Scheme (Scheme Workshop 2004); Ftypes (2011); Rebuilding Racket on Chez Scheme (ICFP 2019).

Indiana University (homepage); the most commits in Typed Racket. Also a co-author of the Fortress specification, see the keynote section.

Earlier State of Racket talks

2023, 2024, 2025.

Releases since RacketCon 2025

Racket v9.0 (parallel threads); v9.1 (February 2026); v9.2 (ffi2); v9.3 (Markdown docs, faster Check Syntax); Rhombus v1.0 (June 2026, the first stable release) and v1.1.

His Typed Racket papers

Typed Scheme (POPL 2008); Logical Types (under Fu above); Occurrence Typing Modulo Theories (PLDI 2016).

The machine these notes were written on runs Racket 8.15, three releases behind v9.3.

git clone https://github.com/quasarbright/treason && cd treason
raco pkg install --auto --batch      # 16 s; installs rackcheck as a dependency
raco test reader-tests.rkt lang-tests.rkt lsp-tests.rkt

reader-tests.rkt   20 tests passed
lang-tests.rkt     31 tests passed
lsp-tests.rkt     173 tests passed

The install also places treason-language-server in Racket's user bin directory.

A one-clause macro whose right-hand side and body are annotated as expressions:

#lang treason
(define-syntax my-let
  (syntax-rules () [(_ x rhs:expr body:expr) (let ([x rhs]) body)]))
(define total 10)
(my-let n (+ total 1) (* n 2))

Run with racket good.tsn, it prints 22. Then drop the body from the macro use and add an unrelated error:

#lang treason
(define-syntax my-let
  (syntax-rules () [(_ x rhs:expr body:expr) (let ([x rhs]) body)]))
(define total 10)
(my-let n (+ total 1))
(define also-bad unbound-name)

$ racket broken.tsn
treason: 2 errors
  5:1: my-let: no pattern matched
  6:18: unbound-name: unbound identifier

Both errors at once. Racket's expander would stop at the first.

The language server can be driven in-process, the way the project's own lsp-tests.rkt does: open the document through server% and send it LSP requests. Three queries on total inside the my-let use, against three versions of the program. Positions are zero-based, counted from the line after #lang.

well-formed use, annotated (rhs:expr body:expr)
  goto-definition on `total` inside the use => definition at line 2, chars 8-13
  find-references on the definition         => the use at line 3, chars 13-18
  autocomplete at `total` inside the use    => ("my-let" "total")
broken use (body missing), annotated
  diagnostic: unbound-name: unbound identifier
  diagnostic: my-let: no pattern matched
  goto-definition on `total` inside the use => definition at line 2, chars 8-13
  find-references on the definition         => the use at line 3, chars 13-18
  autocomplete at `total` inside the use    => ("also-bad" "my-let" "total")
broken use (body missing), NOT annotated (rhs body)
  diagnostic: my-let: no pattern matched
  diagnostic: unbound-name: unbound identifier
  goto-definition on `total` inside the use => ()
  find-references on the definition         => ()
  autocomplete at `total` inside the use    => ()

With the annotations, all three services work inside a macro use that matched no clause. Without them, all three go silent. The annotation is the whole difference, which is the talk's claim.

All in expander.rkt:

Lines 39–40 and 724–781

(~var x expr) and its shorthand x:expr are a pattern form that syntax-rules does not have. annotated-pvar is a match expander that recognises both.

Lines 993–1018, match-pattern

an annotated pattern variable always matches, binds like an ordinary one, and also records the syntax it matched in the result's ose-stxs list (ose is optimistic subexpression expansion). An unknown syntax class binds but records nothing. A plain pattern variable records nothing.

Line 1056 onward

on a pair, the matcher recurses into both sides even when the first fails, so every annotated subexpression in the use is collected, not only those before the failure.

Lines 919–953, try-patterns

if no clause matches, it ranks clauses by how far matching got (progress<?, lines 956–979), keeps the clauses tied for furthest, and takes the intersection of their annotated subexpressions. It raises an ose-error carrying those subexpressions.

Line 396

in an expression context the catcher expands them at once, because every binding is already known.

Lines 570–600

in a definition context they are held until pass 2, when every binding in the context is known, and expanded then.

So the decision is: expand only what the macro's author marked as an expression, from the clause or clauses that got furthest, and only once the scope is complete. The talk script (racketcon/script.md, line 138) names the failure mode: if an argument is missing, positions shift and the matcher may treat the wrong subform as the expression.

syntax/parse (Culpepper and Felleisen, Fortifying Macros, ICFP 2010)

the x:expr notation is syntax/parse's syntax-class annotation. In syntax/parse the class drives error messages; in Treason it also tells the expander which subforms are expressions it can expand on its own. The talk script (line

1. says you have to annotate the same way in syntax/parse to get good

errors.

syntax-spec (Ballantyne, Gamburg and Hemann, ICFP 2024)

Treason only knows one syntax class, expr. The talk ends (script, lines 152–170) on syntax-spec as the way to say more: a grammar for the macro's own nonterminals, such as patterns, and its binding rules, which would let the same recovery work inside a pattern language. The slides credit Michael Ballantyne as co-developer (racketcon/slides.rkt, line 94).

The papers' URLs and the syntax-spec author list are from the program survey above (search only), not opened here.