Design Decisions & Trade-offs¶

Philosophy¶

Prove is an intent-first language. Every function declares its intent — a verb names the purpose, contracts state the guarantees, and explain documents the reasoning — before a single line of implementation is written. The compiler then enforces that the implementation matches the declared intent.

The programmer remains the author — the compiler is a deterministic assistant that enforces what you declared. Intent comes first: the verb names the purpose, contracts state the guarantees, explain documents the reasoning. The type system serves this intent enforcement, moving correctness checks from runtime to compile time and generating tests from the code you already write. Most bugs are type errors in disguise — give the type system enough power and they become almost impossible.

Implementation Decisions¶

File Extension: .prv¶

Investigated .pv, .prove, .prf, .pr, and .prv. Chosen: .prv — short, reads naturally as "Prove", and has no conflicts with existing programming languages or developer tooling.

Prototype Implementation: Python¶

The compiler POC is implemented in Python (>=3.11). The goal is to validate the language design and prove out the compilation pipeline before rewriting in a systems language.

Compilation Target: Native Code¶

As close to the CPU as possible. The compiler does the heavy lifting at compile time so the output is fast and memory-efficient. Target: native code via C emission compiled by gcc/clang. An earlier ASM backend (x86_64) was prototyped at v0.2 and archived — C emission provides better portability and optimization. No VM, no interpreter for production output.

First POC: Self-Hosting Compiler¶

The first program written in Prove will be the Prove compiler itself. The bootstrap path: (1) write a complete compiler in Python, (2) use it to compile a Prove compiler written in Prove. This exercises the type system (AST node types, token variants), verb system (transforms for pure passes, inputs for file reading, outputs for code emission), pattern matching (exhaustive over AST nodes), and algebraic types — proving the language works by compiling itself. Self-hosting is the strongest possible validation: if Prove can express its own compiler, it can express anything.

AI-Resistance: Fundamental¶

AI-resistance features (implementation explanations, intent declarations, narrative coherence, context-dependent syntax, semantic commits) are mandatory and fundamental to the language identity, not optional extras. requires and ensures are hard rules the compiler enforces automatically. explain documents the chain of operations in the implementation using controlled natural language — with ensures present, references are verified against contracts and row count must match the from block.

Comptime: IO Allowed¶

Compile-time computation (comptime) allows IO operations. This enables reading config files, schema definitions, and static assets at compile time. Files accessed during comptime become build dependencies — changing them triggers recompilation. This may be revisited if reproducibility concerns arise.

CLI-First Toolchain: prove¶

The prove CLI is the central interface for all development:

prove build              # compile the project (mutation testing runs by default)
prove build --debug      # compile with debug symbols
prove build --no-mutate  # compile without mutation testing
prove test               # run auto-generated + manual tests
prove check              # type-check without building
prove format             # auto-format source code
prove format --status    # check formatting without modifying
prove lsp                # start the language server
prove new <name>         # scaffold a new project

Syntax Philosophy¶

No shorthands. No abbreviations. Full words everywhere. The language reads like English prose where possible. Since it is inherently a hard-to-learn language (refinement types, implementation explanations, effect tracking), simplicity is maximized wherever possible. If something can be simple, it must be. The compiler works for the programmer, not the other way around.

Secondary Priorities (Deferred)¶

• Calling Prove from other languages — deferred until the FFI story is more mature.
• Method syntax — deferred. All function calls use function(args) form. No object.method() dot-call syntax. Keeps the language simple and avoids dispatch complexity. Field access (user.name) is unaffected.

Concurrency — Structured Concurrency¶

Prove provides structured concurrency through the async verb family (detached, attached, listens) backed by stackful coroutines (prove_coro). Because pure verbs (transforms, validates, reads, creates, matches) guarantee no shared mutable state, the compiler enforces safe concurrency boundaries.

Thread-based par_map, par_filter, and par_reduce are available for pure verbs, running a pthreads-backed thread pool with automatic core detection. They are restricted to pure verbs at compile time — IO and async verbs are rejected. See Parallel Iteration.

The verb system enforces purity boundaries — pure verbs cannot make IO calls, and the compiler rejects violations at compile time.

Error Handling — Errors Are Values¶

No exceptions. Every failure path is visible in the type signature. Uses ! for error propagation. Panics exist only for violated assume: assertions at system boundaries — normal error handling is always through Result values.

main()!
from
    config as Config = read_config("app.yaml")!
    db as Store = connect(config.db_url)!
    serve(config.port, db)!

Zero-Cost Abstractions¶

• Pure functions auto-memoized and inlined
• Region-based memory runtime; per-function scoping is upcoming
• Use-after-move detection for Own modifier; comprehensive tracking is upcoming
• No GC pauses, predictable performance
• Native code output

Pain Point Comparison¶

Trade-offs¶

An honest assessment of the costs:

1. Compilation speed — Proving properties is expensive. Incremental compilation and caching are essential. Expect Rust-like compile times, not Go-like.
2. Learning curve — Refinement types, verb purity, and formal contracts are unfamiliar to most developers. The compiler's suggestions help, but there's still a ramp-up.
3. Ecosystem bootstrap — A new language needs libraries. A C FFI and a story for wrapping existing libraries is a secondary priority, deferred until the core language is stable.
4. Not every property is provable — For complex invariants the compiler falls back to runtime property tests, which is still better than nothing but not a proof.

The core bet: Making the compiler do more work upfront saves orders of magnitude more time than writing and maintaining tests by hand.

AI Transparency¶

Prove is built with honesty about where AI tools are and aren't used.

What is human-authored¶

The Prove language itself — its syntax, semantics, type system, intent verbs, contract model, explain verification, AI-resistance mechanisms, refinement types, and every other novel design idea — is entirely human-invented. All .prv source code (including the planned self-hosted compiler) is written by humans.

Where AI tools help¶

AI tools have been used as implementation aids for the surrounding tooling:

• Bootstrap compiler — the Python CLI, checker, emitter, and supporting infrastructure
• C runtime — the stdlib implementations backing binary functions
• Documentation — writing and maintaining these docs
• Editor integration — tree-sitter grammar, Pygments lexer, Chroma lexer

No single AI tool is credited. Multiple LLMs and open source models have been used throughout development as conceptual partners and coding assistants.

After self-hosting¶

Once the compiler is self-hosted (V2.0, written in Prove and compiled by the V1.0 bootstrap), AI involvement will be limited to documentation maintenance and conceptual discussion. The self-hosted compiler will be human-authored Prove code.

Licensing reflects this¶

The language and .prv source code are covered by the Prove Source License v1.0, which prohibits use as AI training data. The AI-assisted tooling (bootstrap compiler, docs, lexers) is licensed under Apache-2.0. This separation ensures legal clarity: the parts built with AI help use a license compatible with that workflow, while the human-authored language retains its protections.

Inspirations¶

Prove draws from many languages but combines their ideas into something none of them offer: intent-first programming, where every function declares its purpose, guarantees, and reasoning before the implementation begins. The languages below shaped individual features — the verb system, the contracts, the type safety — but the synthesis is uniquely Prove's.

Contributing¶

The Gitea instance at code.botwork.se/Botwork/prove is a paid service for issue creators.

Developers who want contributor access can reach out to magnusknutas[at]botwork.se.

Development Setup¶

To set up your development environment, run ./scripts/dev-setup.sh from the workspace root to install all dependencies. If a tool or package is missing during development, run the script first. If it's still missing after running the script, add the dependency to dev-setup.sh.