One Parser to Rule Them All

April 2026

Prove v1.3.0 ships a major architectural milestone: the legacy recursive-descent parser is gone.
Tree-sitter is now the sole parser for every stage of the compiler — syntax checking, linting,
code generation, and the LSP. Alongside that migration come new verbs, better diagnostics,
and the foundation for lint-driven code quality.

---

Tree-sitter as the only parser

Since v1.2.0 the tree-sitter-prove grammar has been the source of truth for Prove syntax, but the
old hand-written parser still ran in parallel as a fallback. That dual-parser setup is over.

The recursive-descent parser has been removed entirely. Tree-sitter now drives:

• Syntax checking — parse errors come directly from the tree-sitter CST, with precise
  span information and AST error origin tracking.
• Lint checking — a new lint pass runs in the same check pipeline, so proof check
  now catches both syntax and style issues in a single invocation.
• Code generation — the C emitter reads from the tree-sitter AST, removing an entire
  class of “parser A sees it differently from parser B” bugs.

This is a big simplification. One grammar, one parser, one source of truth.

reads becomes derives

The reads verb never quite said what it meant. A function that reads a Text to produce
an Integer isn’t really reading — it’s deriving a new value from existing data.

In v1.3.0 the verb is renamed to derives across the language, standard library, and
documentation. The semantic contract is unchanged: same-type or narrowing transformation,
no allocation, no failure. The name just fits better.

New verb: dispatches

v1.3.0 introduces dispatches for functions that route to different implementations based
on their input. Where derives transforms and creates constructs, dispatches selects.

Verb names are also now mangled in the generated C output, producing cleaner symbol names
in debuggers and profilers.

Native binary catches errors before Python

The proof CLI is the native compiler tool.
Until now it delegated all checking to the Python compiler via FFI. In v1.3.0 the native
binary runs its own tree-sitter-based check pass
before invoking Python — catching errors instantly.

The native check currently catches three diagnostic classes:

• E100 — Syntax errors — tree-sitter ERROR nodes are
  matched and narrowed by parent context (root, module, lookup) to produce targeted messages.
• E210 — Missing type or module — detects undeclared
  modules and types at the declaration level before the full type checker runs.
• E379 — Malformed lookup rows — each row in a
  Lookup table is statically validated against the
  type declaration’s column types.

If the native pass finds errors, it reports them immediately and never starts Python. If it
passes, the full compiler pipeline runs as before.
This is the first step toward a fully native proof check and proof build — more diagnostics will move into
the native binary in future releases.

Linting infrastructure

The compiler now has a dedicated lint pass integrated into the check pipeline. This is the
scaffolding for future code-quality rules — currently focused on structural checks, with
more rules planned for upcoming releases.
The infrastructure to code analysis is in place and that means we can now start moving the python linter into the native proof binary and the first steps towards the bootstrap is on the way!

Implemented diagnostics

Beyond the three native-pass errors above, the Python compiler also gained diagnostic improvements:

• Option<T> match arms — match expressions mixing Unit and value returns now correctly
  produce Option<T> instead of a confusing type error.
• IO requires guards — inputs/outputs/dispatches functions with requires contracts
  now emit runtime guard checks, catching contract violations at the boundary.

Upgrading

curl -sSf https://code.botwork.se/Botwork/prove/raw/branch/main/install.sh | sh

Or if you already have Prove installed:

pip install --upgrade prove-lang

The reads → derives rename is a breaking change for user code. Update your verb declarations — the compiler will tell you exactly which lines need attention.

---

Full changelog on the releases page. Browse the source code, read the documentation, or follow the tutorial to get started.

You can also join the chat #prove (just do a /knock and you will be let in ASAP)