Prove v1.1.0

Prove v1.1.0 is here, and it’s a significant leap forward for the Prove programming language. This release introduces structured concurrency as a first-class language feature, adds three powerful stdlib modules for building interactive applications, and ships the proof CLI as a single binary for effortless onboarding. Whether you’re building terminal-based tools, graphical interfaces, or concurrent systems, v1.1.0 delivers the primitives you need — with zero external dependencies.

Structured Concurrency: Async Verbs as Language Primitives

Prove v1.0 distinguished between pure verbs (no side effects) and IO verbs (impure operations). v1.1 expands this model with a third family: async verbs. These aren’t library functions or convenience wrappers — they’re language-level primitives enforced by the compiler, just like the existing restrictions on pure verbs.

The async verb family includes four variants, each representing a distinct concurrency model:

This design mirrors the existing error-handling syntax. Just as ! propagates failures, the & marker at the call site indicates async behavior. Calling fetch_data()& spawns a coroutine; calling fetch_data()! propagates an error. Both are explicit, both are statically checked, and neither introduces hidden control flow.

The implementation uses prove_coro stackful coroutines based on ucontext_t on POSIX systems, paired with prove_event for the event queue. This is cooperative scheduling — no threads, no preemption, and fundamentally no data races. Every async verb yields voluntarily, making race conditions a compile-time impossibility rather than a runtime concern.

For teams building concurrent systems, this means you get the safety of structured concurrency (think Go’s goroutines or Kotlin’s coroutines) with Prove’s existing guarantees around purity and IO separation. The compiler enforces the rules; you just write business logic.

Building Interactive Applications: Terminal, Graphic, and UI Modules

Beyond concurrency, v1.1 adds three stdlib modules purpose-built for interactive applications: Terminal, Graphic, and UI. These modules enable building terminal user interfaces (TUI) and graphical user interfaces (GUI) without any external dependencies.

Terminal: Zero-Dependency TUI

The Terminal module exposes ANSI escape code primitives directly: raw mode, cursor positioning, screen clearing, and terminal size queries. There’s no ncurses, no termbox, no external bindings — just pure Prove code calling platform primitives.

Here’s a complete todo list application using the `renders` verb:

renders interface(registered_listens_verbs List)
  event_type TodoEvent
  state_init TodoState([TodoItem("Learn Prove", false, 0)], 0)
from
    Draw(state) =>
    clear()
      terminal(0, 0, "=== Todo List ===")
      each(state.items, |item| terminal(0, item.pos + 3, checkboxes(item, state)))
    Exit(state) =>
      cooked()
      Unit

The renders verb owns the event loop and manages mutable state. Each arm (Draw, Exit) handles a specific event type. Self-dispatch — calling Draw(state) after a state change — re-enqueues a draw event to update the screen. The result is a clean, declarative UI pattern that compiles down to efficient terminal I/O.

Graphic: Immediate-Mode GUI

For graphical applications, the Graphic module wraps SDL2 and Nuklear for immediate-mode rendering. Windows, buttons, labels, text inputs, checkboxes, sliders, and progress bars are all available as simple function calls within a renders loop:

renders app(registered_attached_verbs List)
  event_type CounterApp
  state_init CounterState(0)
from
    Draw(state) =>
      window("Counter", 400, 300)
      label(f"Count: {string(state.count)}")
      match button("Increment")
        true =>
          state.count += 1
          Draw(state)
        false => Draw(state)
    Exit(state) => Unit

The backend is auto-detected from the event type chain: if your event type extends TerminalAppEvent, the Terminal backend is used; if it extends GraphicAppEvent, the SDL2/Nuklear backend takes over. Same renders verb, same structure, different runtime — giving you flexibility to target both TUI and GUI from a unified codebase.

Event Translation with listens

The listens verb translates raw platform events (key presses, mouse movements, window events) into application-specific events. A new LookupPattern syntax makes pattern matching readable and expressive:

listens on_key(attached_verbs List) TodoEvent
  event_type KeyDown
  state_type TodoState
from
    Key:Escape => Exit(state)
    Key:"k" => Draw(state)
    Key:Space => ToggleDone()
    _ => Tick(state)

The LookupPattern supports multiple resolution strategies: by variant (Key:Escape), by name (Key:"k"), or by raw keycode (Key:27). This pattern extends to other domains — for example, Color:Red, Color:"#FF0000", or Color:31 all resolve to the same value. The result is a uniform, readable syntax for all kinds of lookups.

The proof CLI: One Binary to Rule Them All

Building Prove code just got simpler. The compiler is now distributed as a single proof binary with a batteries-included command suite:

proof new hello # scaffold a project
proof check # type-check, lint, verify
proof build # compile to native binary
proof test # run contract tests
proof format # format source

Installation is a one-liner:

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

The installer detects your platform (Linux x86_64, macOS aarch64), downloads the appropriate binary, and places it in ~/.local/bin/. Use --version v1.1.0 for a specific release or --prefix /usr/local/bin to install system-wide.

Language Additions: Compound Assignment and Constants

Two small-but-mighty additions ship with v1.1:

Compound assignment operators — +=, -=, *=, /= — are now supported. These are primarily useful for mutable state updates in renders and listens arms, where you’re modifying state in place rather than constructing new values.

The constants import verb lets you import named constants from modules:

module MyApp
  Math constants PI TAU

This keeps the namespace clean while giving you access to values that shouldn’t be functions.

LSP Improvements: Real Cross-File Navigation

Go-to-definition now resolves not just functions and types, but also local variables, function parameters, imported constants, and cross-file symbols. Jump to a function imported from another module, and the language server opens the source .prv file directly. This makes navigation in larger codebases significantly smoother.

Editor Support: Grammar Updates

Tree-sitter and Pygments grammars have been updated with async verbs (attached, detached, listens, renders), import verbs, and the constants keyword. Syntax highlighting works out of the box in Neovim, VS Code (via tree-sitter), and MkDocs/Sphinx documentation.

Benchmarks: Prove vs Python vs Rust

Five new benchmark examples ship with the release, each with implementations in Prove, Python, and Rust for direct comparison:

• Base64 encoding
• Brainfuck interpreter
• JSON parsing
• Matrix multiplication
• Prime sieve

Find them in the examples/ directory of the Prove repository. These benchmarks let you evaluate Prove’s performance against established languages in real-world scenarios.

Internal Improvements

The v1.1 release isn’t just about new features — internal improvements make the codebase healthier:

• Removed 23 unused functions and methods, reducing approximately 378 lines of dead code
• Optimizer improvements: skip memoization for struct, Option, and Result parameters; improved higher-order function reference tracking in runtime dependency analysis
• Cross-platform release pipeline: Linux x86_64 and macOS aarch64 binaries built and published automatically, with Python wheel uploads for the prove-py package

Getting Started with Prove v1.1.0

Ready to try structured concurrency and interactive UIs in Prove? Install the release:

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

Or clone and install from source:

git clone https://code.botwork.se/Botwork/prove && cd prove
pip install -e prove-py/[dev]

Explore the new async verbs, build a terminal app or a GUI, and experience what structured concurrency feels like when it’s baked into the language itself.

Full release notes, binaries, and additional resources are available on the v1.1.0 release page.

—

Tags: Prove

Please leave this field empty

Could we add you to our mailing list!

We don’t spam! Read our privacy policy for more info.

Check your inbox folder to confirm your subscription (lets pretend we never heard of spam for legit emails).