Syntax Reference¶

Naming¶

• Types, modules, and classes: CamelCase — Shape, Port, UserAuth, NonEmpty, HttpServer
• Variables and parameters: snake_case — port, user_list, max_retries, db_connection
• Functions: snake_case — area, binary_search, get_users
• Constants: UPPER_SNAKE_CASE — MAX_CONNECTIONS, LOOKUP_TABLE, DEFAULT_PORT
• Effects: CamelCase — IO, Fail, Async

The compiler enforces casing. Wrong case is a compile error, not a warning. UPPER_SNAKE_CASE indicates a compile-time constant — no const keyword needed.

Modules and Imports¶

Each file is a module. The filename (without extension) is the module name in CamelCase. The module block is mandatory and contains all declarations/metadata: narrative, imports, types, constants, and invariant networks. Functions remain top-level:

module InventoryService
  narrative: """Products are added to inventory..."""
  Text validates length
  Auth validates login transforms login
  Http inputs request session

  type Product is
    sku Sku
    name String

  MAX_CONNECTIONS as Integer = 1024

  invariant_network Accounting
    total >= 0

A verb applies to all space-separated names that follow it. Commas separate verb groups. Multiple verbs for the same function name import each variant. The verb is part of the function's identity — see Functions & Verbs for details.

Foreign Blocks (C FFI)¶

Modules can declare foreign blocks to bind C functions. Each block names a C library and lists the functions it provides with their parameter types and return types:

module PyEmbed
  narrative: """Embed a Python interpreter for scripting support."""

  foreign "libpython3"
    py_initialize() Unit
    py_finalize() Unit
    py_run_string(code String) Integer

Foreign block names must be snake_case — Prove's naming rules apply even to C bindings. Libraries whose C API uses other conventions (like libpython3's Py_Initialize) need thin C wrapper functions that follow snake_case naming before they can be declared in a foreign block.

Foreign functions are raw C bindings — wrap them in a Prove function with a verb to provide type safety and contracts:

outputs run(code String)!
from
    py_initialize()
    result as Integer = py_run_string(code)
    py_finalize()
    match result
        0 => Unit
        _ => console("script exited with non-zero status")

The string after foreign is the library name passed to the linker ("libm" links -lm). Known libraries get automatic #include headers:

For libpython3 and libjvm, the compiler resolves include paths and linker flags in this order:

1. Environment variables — PROVE_PYTHON_CFLAGS / PROVE_PYTHON_LDFLAGS (or PROVE_JVM_CFLAGS / PROVE_JVM_LDFLAGS)
2. pkg-config — queries python3-embed or jni
3. Fallback — plain -lpython3 or -ljvm

Environment variables are the recommended approach for platform-specific paths (Homebrew, Frameworks, custom installs) since they keep prove.toml portable:

# macOS Homebrew example
export PROVE_PYTHON_CFLAGS="-I/opt/homebrew/opt/python@3.13/Frameworks/Python.framework/Versions/3.13/include/python3.13"
export PROVE_PYTHON_LDFLAGS="-L/opt/homebrew/opt/python@3.13/Frameworks/Python.framework/Versions/3.13/lib/python3.13/config-3.13-darwin -L/opt/homebrew/lib -lpython3.13 -lintl -ldl -framework CoreFoundation"

The naming convention is PROVE_<LIB>_CFLAGS / PROVE_<LIB>_LDFLAGS, where <LIB> is the library name with the lib prefix and trailing version digits stripped (libpython3 → PYTHON, libjvm → JVM).

For non-foreign flags (custom include paths, extra libraries), use c_flags and link_flags in prove.toml:

[build]
c_flags = ["-I/usr/local/include"]
link_flags = ["-L/usr/local/lib", "-lm"]

Blocks and Indentation¶

No curly braces. Indentation defines scope (like Python). No semicolons — newlines terminate statements. Newlines are suppressed after operators, commas, opening brackets, ->, =>.

Primitive Types¶

Every type uses its full name. No abbreviations. Type modifiers use bracket syntax Type:[Modifier ...] for storage and representation concerns. Value constraints belong in refinement types (where), not modifiers.

See Type System — Type Modifiers for the complete reference.

Type Definitions¶

Types live inside the module block, defined with type Name is:

module Main
  type Shape is
    Circle(radius Decimal)
    | Rect(w Decimal, h Decimal)

  type Port is Integer:[16 Unsigned] where 1 .. 65535

  type Result<Value, Error> is Ok(Value) | Err(Error)

  type User is
    id Integer
    name String
    email String

Literals¶

Prove has several literal syntaxes for different types:

count as Integer = 42           // Integer literal
precision as Decimal = 3.14    // Decimal literal (arbitrary precision)
speed as Float = 9.8f          // Float literal (IEEE 754, requires 'f' suffix)
flag as Boolean = true
greeting as String = "Hello"
char as Character = 'x'
pattern as Regex = r"\d+"
path as Path = /users/alice/

The f suffix on floating-point literals (like 9.8f) creates a Float type, suitable for IEEE 754 operations like Math.sqrt and Math.floor. Without the suffix (like 3.14), you get a Decimal type for exact decimal arithmetic.

Variable Declarations¶

Variables use name as Type = value. The as keyword reads naturally: "port, as a Port, equals 8080".

port as Port = 8080
server as Server = new_server()
config as Config = load("app.yaml")!
user_list as List<User> = users()!

Variables are immutable by default. Mutability is a type modifier — it's a storage concern, like size and signedness:

counter as Integer:[Mutable] = 0
counter = counter + 1

Type Inference with Formatter Enforcement¶

The compiler infers types when unambiguous, but prove format always inserts explicit type annotations. This means you can write clean code during development, and the formatter makes it explicit before commit.

// What you write:
port = 8080
server = new_server()
users = query(db, "SELECT * FROM users")!

// What `prove format` produces:
port as Integer = 8080
server as Server = new_server()
users as List<User> = query(db, "SELECT * FROM users")!

The LSP shows inferred types on hover, so you always know what the compiler deduced. Function signatures are always explicit — inference only applies to local variables.

The language encourages explicit types — the formatter enforces them. But you're never blocked from writing code because you can't remember whether it's List<Map<String, User>> or Map<String, List<User>>.

Keywords¶

Every keyword in Prove has exactly one purpose. No keyword is overloaded across different contexts. This makes the language predictable and parseable by humans without memorizing context-dependent rules.

For a complete keyword reference with links to detailed documentation, see the Keyword Reference in the Type System document.