Skip to content

RCE language specification, draft 0.5

1. Notation and conformance

This section fixes how the rest of the spec is written and what it means for an implementation to follow it. EBNF (extended Backus-Naur form) is a notation for grammars; an inference rule states that a conclusion holds when its premises hold. For example Option = "[" Expression "]" . says an option is an expression in brackets.

Grammar notation. EBNF in the style of the Go specification:

Grammar Production, Expression, Term, Factor, Group, Option, Repetition
Production=name "=" Expression "." .Expression=Term { "|" Term } .Term=Factor { Factor } .Factor=name ∣ token [ "…" token ] ∣ Group ∣ Option ∣ Repetition .Group="(" Expression ")" .Option="[" Expression "]" .(0 or 1)Repetition="{" Expression "}" .(0 or more)\begin{array}{rcl}\textsf{Production} & = & \texttt{name}\ \texttt{"="}\ \texttt{Expression}\ \texttt{"."}\ . \\ \textsf{Expression} & = & \texttt{Term}\ \{\ \texttt{"|"}\ \texttt{Term}\ \}\ . \\ \textsf{Term} & = & \texttt{Factor}\ \{\ \texttt{Factor}\ \}\ . \\ \textsf{Factor} & = & \texttt{name}\ |\ \texttt{token}\ [\ \texttt{"…"}\ \texttt{token}\ ]\ |\ \texttt{Group}\ |\ \texttt{Option}\ |\ \texttt{Repetition}\ . \\ \textsf{Group} & = & \texttt{"("}\ \texttt{Expression}\ \texttt{")"}\ . \\ \textsf{Option} & = & \texttt{"["}\ \texttt{Expression}\ \texttt{"]"}\ .\quad\textcolor{gray}{(0\ \text{or}\ 1)} \\ \textsf{Repetition} & = & \texttt{"\{"}\ \texttt{Expression}\ \texttt{"\}"}\ .\quad\textcolor{gray}{(0\ \text{or}\ \text{more})} \\\end{array}
Plain text of this block
Production  = name "=" Expression "." .
Expression  = Term { "|" Term } .
Term        = Factor { Factor } .
Factor      = name | token [ "…" token ] | Group | Option | Repetition .
Group       = "(" Expression ")" .
Option      = "[" Expression "]" .      (0 or 1)
Repetition  = "{" Expression "}" .      (0 or more)

Lower-case names are syntactic productions, UPPER names are tokens, and quoted strings are literal tokens. NEWLINE, INDENT and DEDENT are produced by the layout pass (2.6).

Judgment notation. Inference rules are written

Typing rules Name
premise1…premisenconclusion  [Name]\dfrac{\begin{array}{c}\text{premise}₁\qquad …\qquad \text{premise}ₙ\end{array}}{\begin{array}{c}\text{conclusion}\end{array}}\;\textsf{[Name]}
Plain text of this block
  premise₁   …   premiseₙ
  ───────────────────────── [Name]
         conclusion

Γ is a typing context (name ↦ type, mode), Δ a context of live borrows, Σ the declaration environment (types, kinds, traits, events, errors, regions). "iff" means if and only if.

Conformance. An implementation (a) refuses every text that is not in the language of section 3, or that breaks a rule of section 7, with a diagnostic naming the rule; (b) for every accepted program, computes δ, λ and the fold of section 6 exactly, including every edge in 6.3. Behavior the spec does not define does not exist: there is no "undefined behavior" and no "implementation-defined" result. The only implementation freedom is cost (time, memory, energy), never value.

Built from spec commit 49fa9af. Code cells run the reference checker rce-check, written in Rust and compiled to WebAssembly, inside your browser; nothing is sent to a server. Read-aloud uses the Kokoro-82M model (Apache-2.0), served from this site and run in your browser.