Tauto
← All articles
/ ENGINEERING NOTES

For Macro Lovers: Could Tauto Have the World's Most Powerful Macro System?

Hygienic DSLs, typed transformations, proof tactics, and effect-restricted expansion in one macro system.

tautomacrosdslformalverification

Tauto combines a dependently typed proof system with a runtime featuring algebraic effects and ownership. This article introduces its macro system.

“The world's most powerful” is a bold claim for a title. The aim is to bring everything I want from macros into a single design:

  • Add new syntax and DSLs as libraries, complete with registered formatters and syntax highlighting.
  • Write macros that transform code based on its types and macros that build proofs, called tactics, using the same mechanism.
  • Keep expansion hygienic, so macros do not capture the caller's variables.
  • Run untrusted macros without giving them file access, without unbounded execution, and without compromising proof soundness.

Tauto on GitHub

Macros are ordinary functions that return syntax values

Tauto macros are ordinary functions, rather than programs in a separate macro or template language. They take and return syntax values, represented by AST data types such as SynExpr and SynStmt, assembled with quote { … } and $x. Calls are always explicit: NAME!(…).

Whatever a macro produces, the expanded program goes through the same path as a handwritten program: the kernel and a second, independently implemented kernel. You do not need to trust the macro's generation logic to preserve type or proof soundness.

Macro kinds and when to use them

There are four kinds of macros. The function's input type alone determines the kind. There is no keyword such as typed macro.

  • Syntax macro: takes a typed AST generated from a grammar. Call it as name!(`…`) to introduce notation or a DSL.
  • Untyped macro: takes SynExpr. Call it as name!(a + b) to reinterpret an expression.
  • Typed macro: takes Judgement. Call it as name!(e) to transform code using its type and context.
  • Tactic: takes ProofStep. Call it as by name!(…): G { … } to automate proofs.

Syntax macros: write in your own grammar

A syntax macro parses its input using a grammar declared with syntax!. As an example, here is swap!, which swaps two variables.

syntax!(swp, ```par
%start Pair
%%
Pair: Name Name;
Name: /[\p{L}_][\p{L}\p{N}_]*/;
```) => struct Pair, fn parse

pub macro fn swap(p: swp::Pair): List(SynStmt) {
  let a := Syn::ident(p.name)
  let b := Syn::ident(p.name_2)
  quote stmts {
    let tmp := $a
    $a := $b
    $b := tmp
  }
}

The grammar lives in a fenced block tagged par. It automatically generates a typed AST called swp::Pair, which becomes the macro function's input.

After =>, the source lists the exact kinds and names of the declarations that will be generated. You do not need to write these lists by hand: tauto fmt --fill-generated main.taut fills in missing lists and corrects mismatched ones in that file and the files it imports, writing the results back to source.

The list is required for syntax!, inductive_syntax!, attribute macros, and other declaration-generating calls. Generating an unlisted declaration is an error, as is listing a declaration that is not generated. “Why list generated declarations?” below explains why the list remains explicit in the source.

Here is the caller:

import "swap.taut"
var tmp := 1
var other := 2
swap!(`tmp other`)
perform show("tmp", tmp)
perform show("other", other)

$ tauto macro expand main.taut
var tmp := 1
var other := 2
let tmp#1 := tmp
tmp := other
other := tmp#1
perform show("tmp", tmp)
perform show("other", other)

$ tauto run main.taut
tmp = 2
other = 1

The macro's temporary variable tmp becomes tmp#1, avoiding a collision with the caller's tmp. The #1 is a display name; when --write writes the expansion back to source, it becomes an ordinary name that does not collide. This illustrates the hygiene mechanism discussed below. You can inspect expansions at any time with tauto macro expand.

The DSL inside the backtick fences can also have its own formatter and syntax highlighting. Register the functions with with at the end of syntax!:

syntax!(swp, ```par
…
```, with(fmt: swp_fmt, tokens: swp_tokens)) => struct Pair, fn parse

fmt is called when tauto fmt formats the contents of a syntax literal such as swp`…` . tokens is called when the language server highlights it. The grammar author defines swp_fmt and swp_tokens as ordinary Tauto functions. Without registration, the contents are left unformatted and highlighting is inferred from terminal names. More details appear in “Registering formatters and syntax highlighting” below.

Untyped macros: reinterpret an expression

An untyped macro receives anything that parses as a Tauto expression as a syntax value, without type-checking it first. The standard library's nat! reinterprets == as propositional equality = and + as Nat::add, allowing theorem statements to look like mathematical expressions:

theorem add_comm_stmt(a: Nat, b: Nat): nat!(a + b == b + a) { Nat::add_comm(a, b) }

Because it runs before checking, it cannot inspect types. In return, it can accept expressions that would not otherwise type-check, such as an expression using == where that operator is not defined.

Typed macros: inspect types and context

A typed macro receives a checked expression as an opaque Judgement value containing its context, term, type, effect row, and variable usage. It runs only after the declaration containing the call has been checked once without macro expansion. User code never runs in the middle of type inference. This structurally rules out a cycle in which a macro inspects a type and then changes the type based on what it finds.

The output is accepted only if its type is definitionally equal to the original expression's type, its effect row is a subset of the original row, and the entire declaration passes checking again. Ownership, borrowing, and linearity are also checked across the whole expanded declaration. Matching types alone is not treated as a sufficient safety check.

If you also want to preserve meaning, you can choose the Proved result form, which returns a proof of equality e = e' alongside the transformation. The kernel checks that proof.

Tactics: macros that construct proofs

A macro taking ProofStep can be used inside a proof. The kernel checks the term it constructs against the explicitly written goal. Even if a tactic produces an incorrect proof, the kernel decides whether to accept it; the tactic itself does not need to be trusted.

Succ(k) => by rewrite!(Nat::add_comm(a, k)): Succ(Nat::add(a, k)) = Nat::add(Succ(k), a) {
  ⊢ Succ(Nat::add(k, a)) = Nat::add(Succ(k), a) from by rewrite!(Nat::add_succ_left(k, a)) {
    ⊢ Succ(Nat::add(k, a)) = Succ(Nat::add(k, a)) from Refl
  }
}

rewrite! is a standard-library tactic. Since the goal is written at every step, readers can follow the proof without knowing how the tactic is implemented.

Attribute macros: generate declarations

Writing @name!(…) before a declaration lets a macro generate declarations. This is a separate axis from the four kinds above: “attribute macro” describes the call's position, rather than a kind determined by its input type. The macro itself is a syntax macro or an untyped macro.

@mode!(`lookup(rec G, in i, out A) -> Looked { HasFound | HasNone }`) => inductive Looked, fn lookup
inductive Has: (List(Ty)) -> (Nat) -> (Ty) -> Prop { … }

This uses the standard library's mode! to turn the inductive relation below it into a decision function with uniquely determined outputs and a result type carrying a proof of correctness. It cannot transform arbitrary relations: the generator imposes conditions on the shapes of rules it accepts. The kernel checks the generated types and terms as usual.

The list after => names the declarations generated in addition to the original declaration, following the same listing rule. By default, the original declaration remains exactly as written. Rewriting it requires an explicit replace. A handwritten declaration cannot silently turn into something else.

Why list generated declarations?

A declaration-generating macro must list its generated declarations after => at every call. The macro already knows what it generates, so this could seem like something to infer automatically. Requiring it is deliberate: people and AI tools reading the source should be able to trace where a name came from without expanding the macro. Without the list, the origin of Looked or lookup would only become apparent after expansion. A mismatch between the list and the actual output is an error, so stale lists cannot remain unnoticed.

You do not, however, need to write the list by hand:

$ tauto fmt --fill-generated main.taut

This fills in missing or incorrect lists using the fixes suggested by the diagnostics. The completed list is written into the source, where readers can see it without expanding anything.

Hygiene: macros do not capture the caller's names

Identifiers carry both a name and a set of scopes. Each expansion adds and removes a fresh scope on its output. This gives the following behavior:

  • Identifiers introduced by a macro's quote do not capture the caller's variables.
  • Identifiers that came from the input resolve to the bindings intended by the caller.
  • Global names written in the macro refer to declarations in its definition file, even if the caller has declarations with the same names.
  • Intentional capture is possible only through an explicit operation, Syn::ident_like.

Captures are marked as such in tauto macro trace and are prohibited by lint in the standard library. The policy is to make hidden bindings visible.

Using effect analysis to contain macro execution

Macros execute arbitrary code at compile time. Rust procedural macros run with the compiler process's privileges, so they can access files and the network. Tauto restricts this through effect rows in the type system.

A macro function's effect row must be a subset of {macro_error, macro_warn, elab, Div}. A function with any other effect cannot be registered as a macro.

pub macro fn leak(p: swp::Pair): SynExpr ! {macro_error, Div} {
  let _ := read_file("/etc/passwd")
  quote { 1 }
}

FAILED  macro: main.taut:2:10: macro.row: the function of a macro may perform macro_error, macro_warn, elab and Div, and `leak` performs fs_read

Reading a file performs fs_read, which is not allowed in a macro's row, so the macro is rejected. The same applies to networking, environment variables, the clock, randomness, and standard output.

Even if a standard effect were about to execute despite this check, the host running the macro would refuse to handle it and report an error. Directly calling built-in functions that access files or the network is rejected too.

What about infinite loops?

Div marks functions that may diverge. It is allowed in macros so they can use recursion and while, but macro execution is subject to budgets.

pub fn spin(n: i64): i64 ! {Div} { spin(n) }
pub macro fn loopy(p: swp::Pair): SynExpr ! {macro_error, Div} {
  let _ := spin(0)
  quote { 1 }
}

FAILED  macro: main2.taut:2:10: macro.budget_exceeded: macro loopy took more than 10000000 steps

Budgets cover steps per call (10⁷ by default), the total per file (10⁸), expansion depth (64), output nodes (10⁵), and evaluator memory allocations (10⁷). Exceeding one produces a diagnostic and fails that declaration, while checking continues with the next declaration. Huge outputs and chains in which macros keep calling more macros are stopped in the same way. DSL strings are also limited to 1 MiB, and the parsing stack to a depth of 10⁴.

Macros also cannot:

  • Emit axiom, extern, or import, silently extending the set of things that must be trusted.
  • Create a hole such as ?h: syntax values have no constructor for holes.
  • Put include_text! into their output to read a file. Includes run before macro expansion, and only for calls explicitly written in the source.

Even a malicious macro from a dependency can only emit code that could be written by hand, within the allowed effects and execution budgets. Those effects include diagnostics. You can inspect its output with tauto macro expand, and the kernel ultimately checks it.

A powerful syntax-macro system

Write a grammar, get a typed AST and parser

A grammar passed to syntax! automatically produces a typed AST using struct and enum for its nonterminals, together with a parse function that is also usable at runtime. It can even be used directly as a syntax literal, without invoking a macro: math`1 + 2 = 3` produces a math::Eqn value without running a macro.

The grammar notation is the same parol format used by tauto.par, which defines Tauto's own syntax. Users can therefore add their own languages using the same notation used for Tauto itself. Parsing is table-driven. The tables generated from a grammar are ordinary files that can be committed under .tauto-syntax/; the grammar generator does not have to run on every build.

Left recursion: LL(k) and LALR(1)

The default grammar class is LL(k), with lookahead k ≤ 3. Since left recursion is not allowed there, operators are expressed using repetition, such as { Plus Term }.

For more natural left recursion or operator precedence, specify %grammar_type 'LALR(1)' to generate an LALR(1) table:

syntax!(ex, ```par
%start E
%grammar_type 'LALR(1)'
%%
E: E Plus T | T;
T: Num;
Num: /[0-9]+/;
Plus: '+';
```) => enum E, struct T

let r := ex`1 + 2 + 3`

The left-recursive production E: E Plus T works as written. Removing the %grammar_type line makes the grammar LL(k); lookahead conflicts then cause tauto syntax gen to reject it.

Both kinds of tables are generated by programs written in Tauto itself, in Nib: totes/llkgen and totes/lalrgen. The LALR(1) generator is written to construct the same states as lalry, the library used by parol, and tests compare their outputs. This is part of self-hosting Tauto's grammar infrastructure.

Ambiguous grammars are reported as conflicts. They are not accepted by retaining multiple parse results or hiding the ambiguity behind ordered choice. This keeps the typed AST unambiguous.

Syntax errors report locations and expectations

An error inside a DSL points to the actual line and column within the call's string and lists the terminals expected there:

2 + * 3 => error: macro.syntax_error: in calc: expected Num or LParen, found Star

For indented multiline literals, locations are adjusted for the indentation removed during parsing, so they still point to what the user wrote.

Registering formatters and syntax highlighting

syntax! accepts with(fmt: …, tokens: …) to attach functions that handle text in that syntax:

syntax!(layout, ```par
%start Doc
%title "layout"
%%
Doc: Item { Comma Item };
Item: Num | Word;
Num: /[0-9]+/;
Word: /[a-z]+/;
Comma: ',';
```, with(fmt: layout_fmt, tokens: layout_tokens)) => struct Doc, struct Doc_Rep1, enum Item, fn parse

let d := layout`1,2 ,   foo,3`

When tauto fmt finds a literal in this syntax, it calls layout_fmt to format the contents:

let d := layout`1, 2, foo, 3`

layout_fmt and layout_tokens are ordinary Tauto functions that take a list of SynTok values (a token stream including whitespace and comments) or a lossless concrete syntax tree, SynCst. The ranges returned by tokens determine the language server's highlighting. Without a registered function, highlighting is inferred from terminal names.

The only effects these functions may have are Div and macro_error. They cannot access files or other external resources.

$name and ${…} inside a DSL are always highlighted as Tauto, whether or not tokens is registered. Any ranges returned by tokens that overlap these interpolations are trimmed. If the token function fails type checking, reports an error, or returns a range outside the text, the literal falls back to highlighting based on terminal names and gets a warning explaining why.

Formatters are also constrained. Before writing a result back, tauto fmt checks three things, keeping the original text and issuing a warning if any check fails:

  • The result parses as the same syntax.
  • The token sequence, excluding whitespace, is unchanged.
  • Formatting again leaves the result unchanged: the formatter is idempotent.

A formatter bug therefore cannot change tokens or leave the literal unparsable. These checks are not sufficient, however, for syntax where whitespace changes can change meaning, such as an indentation-sensitive grammar. Authors of fmt functions for such grammars still need to handle that carefully.

Embedding Tauto expressions in a grammar

The reserved terminal TautoExpr lets you embed a Tauto expression inside a DSL with ${ … }. The standard library's nat! uses this to embed Tauto expressions in mathematical notation:

pub theorem mul_comm(n: Nat, m: Nat): nat!(`$n * $m = $m * $n`) { … }

$n refers to the variable n, while ${Succ(k)} is an expression. Embedded expressions retain their actual source locations.

Build and prove a language implementation

In addition to the struct/enum AST, inductive_syntax! generates proof-side inductive types, with an ::I suffix such as Expr::I, and conversion functions such as Expr::to_i. You can then state theorems about the AST generated from the grammar.

examples/calc is a small language implementation that reads arithmetic expressions with addition and multiplication from text:

inductive_syntax!(arith, ```par
%start Expr
%title "calc"
%%
Expr: Prod { Plus Prod };
Prod: Atom { Star Atom };
Atom: Num | Paren;
Paren: LParen Expr RParen;
Num: /[0-9]+/;
Plus: '+';
Star: '*';
LParen: '(';
RParen: ')';
```) => enum Atom, struct Expr, … , fn parse, inductive Expr::I, … , fn Expr::to_i, …

$ tauto check examples/calc/proof/calc.taut
10 ok, 0 failed, 0 incomplete; 0 skipped, 124 from imports; axioms: none

Among the properties proved here is calc_run_correct: for any syntax tree, the compiled code runs without a stack underflow and leaves the value represented by that tree on the stack. The proofs check without additional axioms: axioms: none.

Some parts remain unproved. The text-to-tree parser arith::parse and the conversion to_i are outside these proofs. The parser is a driver over the tables produced by the grammar generator, and its correctness has not yet been formally established. There is no formal proof yet that the text has the meaning represented by the tree. What can currently be proved is soundness and completeness from the tree returned by the parser onward. Getting the AST as an inductive type makes it possible to start writing a proof of the parser itself; that proof is not complete.

More useful properties

Every expansion can be traced

Every node generated by a macro carries provenance: its call site, definition site, whether it was generated, and the chain of nested expansions. Diagnostics follow that chain to show which macro introduced what, for example: “x (introduced by expansion of math).”

tauto macro expand [--all | --at LINE:COL | --write | --json] FILE   # inspect or write back the expansion
tauto macro trace [--json | --diff] FILE                    # trace expansion steps
tauto macro inspect FILE --at LINE:COL [--json]
tauto check --json                                           # list expansions

With --write, you can write an expansion back to source and keep a version that no longer uses the macro. All these commands support --json, allowing AI agents to inspect macro expansion programmatically.

Typed macros do not change the declaration environment

Only syntax macros and attribute macros can generate declarations. A typed macro changes only the expression at its call site.

Write typing judgments in a DSL

In examples/lambda, theorems about typing and reduction in the simply typed lambda calculus can be written directly in the calculus's notation. A syntax named lc parses contextual judgments using a grammar containing |- and ~>*, and is also used inside proofs:

pub theorem k_star(): lc!(`(fun x: unit. fun y: unit. x) star ~>* fun y: unit. star`) { … }

Macro execution is ordered by file

You can only use macros defined in an earlier file or in a dependency tote (a package). Defining and using a macro in the same file is an error. This makes the timing of macro execution visible at a unit a reader can understand.

Deliberate restrictions

Here are the restrictions discussed above. These are freedoms found in some other macro systems that Tauto deliberately does not provide:

  • Access files, the network, environment variables, time, randomness, or standard output from a macro. Instead, include_text! reads a file only at an explicitly written call site.
  • Generate declarations or change the environment from a typed macro. Instead, syntax and attribute macros generate declarations, with the generated names listed in advance after =>.
  • Run a macro in the middle of type inference. Instead, a typed macro receives a checked expression as a Judgement.
  • Put axiom, extern, import, or a hole such as ?h in macro output. Instead, emit code that can be written by hand, subject to these output restrictions.
  • Silently replace a handwritten declaration. Instead, explicitly request replacement with replace.
  • Use a macro in the same file where it is defined. Instead, use a macro from an earlier file or a dependency tote.
  • Silently capture a variable. Instead, explicitly capture it with Syn::ident_like, leaving a trace.
  • Guarantee the output's type when the macro itself is written. Instead, check the expansion with the same checkers used for handwritten code.

Each of these freedoms can be useful. Tauto draws these boundaries to keep the trusted implementation small and expansions readable.

Design priorities

  1. Soundness: do not accept invalid types, proofs, or authority.
  2. Minimalism: minimize concepts, special rules, and trusted implementation.
  3. Composability.
  4. Expressiveness.
  5. Security.
  6. Readability for AI: machine-readable ASTs, types, errors, and expansion steps.
  7. Performance.
  8. Self-hosting.

What is not guaranteed

  • Proving the runtime evaluator correct is planned at the model level in Lean; correspondence with the Rust evaluator is checked by tests. A flaw in the evaluator could break macro isolation.
  • Macros are not prevented from generating code that performs dangerous actions. That code is treated the same way as the equivalent handwritten code, and can be inspected with tauto macro expand.
  • A macro close to a resource budget may succeed or fail differently after an evaluator version change. Usage above 90% of the limit produces a warning.
  • As noted above, the correctness of the grammar-generated parser remains unproved.
  • The language is still experimental. Syntax and diagnostic messages shown here may change.

Summary

  • Macros are ordinary functions returning syntax values. Their input types determine their kinds.
  • Expansions are checked by the same checkers as handwritten code, keeping macros out of the trusted base.
  • Hygiene uses scope sets. Capture requires an explicit operation and leaves a trace.
  • Effect rows prevent file and network access. Macros may use Div, but execution budgets turn nontermination into diagnostics.
  • Writing an LL(k) or LALR(1) grammar gives a syntax macro a typed AST, parser, and syntax literals. Formatters and highlighting can also be registered.
  • inductive_syntax! brings ASTs into the proof world, making it possible to state theorems about language implementations. The parser itself remains unproved.

Tauto on GitHub