Prove¶
An intent-first programming language.
Every function in Prove declares its purpose (verb), guarantees (contracts), and reasoning (explain) before the implementation begins. The compiler enforces that intent matches reality. The vision extends this to the entire development workflow: local, self-contained development where your project's own declarations drive code generation — no external AI services, no black box. The programmer remains the author; the toolchain is a deterministic assistant that works from what you've explicitly declared. This strict intent enforcement also makes Prove naturally resistant to AI — generating semantically correct Prove code requires genuine understanding, not pattern matching. Source code is covered by an anti-training license.
The ensures clause declares hard postconditions — the compiler enforces them automatically. The transforms verb guarantees purity. None of it can be faked by autocomplete.
Why Prove?¶
| Problem | How Prove solves it |
|---|---|
| AI scrapes your code for training | Anti-training license + intent enforcement (binary AST format and semantic normalization planned) |
| AI slop PRs waste maintainer time | Compiler rejects code without explanations and intent |
| Tests are separate from code | Testing is part of the definition — ensures, requires, near_miss |
| "Works on my machine" | Verb system makes IO explicit |
| Null/nil crashes | No null — Option<Value> enforced by compiler |
| "I forgot an edge case" | Compiler generates edge cases from types |
| Runtime type errors | Refinement types catch invalid values at compile time |
| Code without reasoning | explain documents each step using controlled natural language — verified against contracts |
| External AI dependency | Local, self-contained generation from your project's own declarations |
Install¶
Install the latest proof binary:
This detects your platform (Linux x86_64, macOS aarch64), downloads the binary, and installs it to ~/.local/bin/.
Options: --version v1.3.1 for a specific release, --prefix /usr/local/bin for a custom location.
All releases and platform binaries are available on the releases page.
Quick Start¶
# Create a project
proof new hello
# Build and run
cd hello
proof build
./build/hello
# Type-check only
proof check
# Run auto-generated tests
proof test
Language Tour¶
Intent Verbs¶
Every function declares its purpose with a verb. The compiler enforces it. Pure verbs (transforms, validates, derives, creates, matches) cannot perform IO. IO verbs (inputs, outputs, dispatches) make side effects explicit. Async verbs (detached, attached, listens, renders) provide structured concurrency.
validates email(address String)
from
contains(address, "@") && contains(address, ".")
inputs users(db Store) List<User>!
from
query(db, "SELECT * FROM users")!
The same name can exist with different verbs — the compiler resolves which to call from context.
Refinement Types¶
Types carry constraints, not just shapes. See Type System — Refinement Types for the full reference.
type Port is Integer:[16 Unsigned] where 1..65535
type Email is String where r"^[^[:space:]@]+@[^[:space:]@]+\.[^[:space:]@]+$"
type NonEmpty<Value> is List<Value> where len > 0
Contracts¶
requires and ensures are hard rules about the function's interface. explain documents the implementation steps using controlled natural language — verified against contracts when ensures is present.
matches apply_discount(discount Discount, amount Price) Price
ensures result >= 0
ensures result <= amount
requires amount >= 0
from
FlatOff(off) => max(0, amount - off)
PercentOff(rate) => amount * (1 - rate)
No Loops — Functional Iteration¶
Prove enforces functional iteration (map, filter, reduce) over traditional loops.
names as List<String> = map(users, |u| u.name)
active as List<User> = filter(users, |u| u.active)
total as Decimal = reduce(prices, 0, |acc, p| acc + p)
Error Handling¶
Errors are values. ! propagates failures. No exceptions.
main()!
from
config as Config = load("app.yaml")!
db as Store = connect(config.db_url)!
serve(config.port, db)!
Store — Versioned Data Tables¶
Prove includes a built-in Store module for persistent lookup tables with versioning, diffs, and three-way merging. Tables use optimistic concurrency — stale writes fail fast, and conflicts are resolved with user-provided callbacks.
inputs update(path String, name String) StoreTable!
from
db as Store = Store.store(path)!
table as StoreTable = Store.table(db, name)!
// Save — fails if another process wrote a newer version
Store.table(db, table)!
Simple Example¶
Here's a basic function definition that transforms an integer and ensures its output:
For a more comprehensive demonstration of Prove's features, see the Inventory Service Example.
Ecosystem¶
- tree-sitter-prove — Tree-sitter grammar for editor syntax highlighting
- pygments-prove — Pygments lexer for MkDocs and Sphinx code rendering
- chroma-lexer-prove — Chroma lexer for Gitea/Hugo code rendering
Status¶
Prove v1.3.1 is released. Tree-sitter is now the sole parser, the reads verb is renamed to derives, a new dispatches verb is added, verb names are mangled in C output, and the compiler gains a unified linting pass. See the Releases page for details and the Roadmap for what's next (V2.0: self-hosted compiler).
Repository¶
Source code is hosted at code.botwork.se/Botwork/prove.
Contributing¶
Join #prove on Libera.Chat (just do a /knock and you will be let in ASAP) for questions and discussion. For more details, see our Contributing section.
License¶
The Prove language, its specification, and all .prv source code are covered by the Prove Source License v1.0 — permissive for developers, prohibits use as AI training data.
The compiler tooling (bootstrap compiler, documentation, editor integrations) is licensed under Apache-2.0. See AI Transparency for why the licenses differ.