The Pluto Programming Language

Most languages give up at the function boundary. They see your code as isolated units — functions, classes, modules — analyzed in isolation, then stitched together at runtime through reflection, containers, or shared conventions. The compiler type-checks each piece, generates code for each piece, and trusts that you wired everything correctly.

Pluto sees your entire program at compile time. It analyzes the complete call graph, traces error propagation through every path, resolves your dependency graph, and generates a self-contained native binary with all the knowledge baked in. No runtime container. No reflection. No framework discovering your code at startup.

This is whole-program compilation, and it changes everything.

What Whole-Program Compilation Gives You

When the compiler sees your entire program, it can do things that are impossible with separate compilation:

Zero-cost dependency injection. The compiler builds the complete dependency graph at compile time, performs a topological sort, and generates direct allocation and wiring code. There is no container looking up service registrations at runtime. There is no reflection scanning for @Inject annotations. The cost is literally zero — it compiles down to a sequence of calloc calls and pointer assignments in your main() function.

Compiler-inferred error handling. The compiler traces every function call in your program, determines which paths can raise errors, and computes the exact error set for each function. You never write throws or Result<T, E>. The compiler infers fallibility from the complete call graph and enforces handling at every call site. If you forget a ! or catch, the program does not compile.

Dead code elimination. The compiler sees every call site in your program. If you import a module with 50 functions but only call 3 of them, the other 47 don’t make it into your binary. If you wire up a service that’s declared but never used, it doesn’t get allocated. This isn’t LTO doing cleanup after the fact — the compiler knows what you use because it sees all of it.

Monomorphization of generics. The compiler sees every instantiation of every generic type and function across your entire program. It generates exactly the concrete versions you use — Box<int>, Pair<string, float>, Option<User> — and nothing else. No vtables, no boxing, no type erasure. The type parameters are erased at runtime because they were resolved at compile time.

Compile-time proofs. Class invariants are not runtime checks — the compiler proves them at every construction and write site, or compilation fails. The proofs feed back into error handling: a guard that makes a callee’s raise impossible removes the handling obligation at that call site. Whole-program analysis is what makes “every write site” a knowable set.

Placement over logical domains. at domain { expr } runs a computation where it logically belongs; whether that boundary is crossed in-process or over a socket is decided by the deployment binding at startup, not by the code. The compiler checks the boundary contract — wire-shaped values, typed errors, mandatory handling, interface-hash version guards — identically in every plan. A system declaration compiles multiple services as one checked program, one binary per member.

This is the core thesis of Pluto: If the compiler sees your whole program, it can solve problems that otherwise require frameworks, containers, and runtime magic.

What Makes Pluto Different

Language-level dependency injection. Classes declare their dependencies in brackets. The compiler sees every class in your program, builds the full dependency graph, and generates explicit wiring code. At runtime, there is no container, no service locator, no getInstance() calls — just a sequence of allocations in dependency order. This only works because the compiler sees the whole program.

class OrderService[db: Database, cache: Cache] {
    fn get_order(self, id: string) Order {
        return self.db.query(f"SELECT * FROM orders WHERE id = {id}")
    }
}

Compiler-inferred error handling. You never annotate functions as fallible. The compiler walks the complete call graph for your program, discovers every raise statement, traces error propagation through every function call, and computes the exact error set each function can produce. It enforces handling at every call site. If you forget ! or catch, compilation fails. This is only possible with whole-program analysis.

fn process(id: string) string {
    let order = find_order(id)!      // compiler knows find_order can fail
    let receipt = charge(order)!      // compiler knows charge can fail
    return receipt.confirmation       // compiler knows this function can fail
}

The app as a first-class construct. The app declaration is the entry point, the dependency root, and the unit of deployment. It is not a function with a special name – it is a structural declaration that the compiler understands and can reason about.

app PaymentSystem[orders: OrderService, payments: PaymentProcessor] {
    fn main(self) {
        self.orders.process("ORD-42") catch err {
            print("payment failed")
            return
        }
    }
}

Contracts. Classes declare invariants that the compiler proves at compile time — every construction and write site is statically discharged, or compilation fails with a diagnostic naming the missing fact. No runtime invariant checks exist inside the program; the only runtime validation is at wire-decode boundaries, where external data is testimony rather than proof. Functions declare requires preconditions, runtime-checked at entry and assumed by the prover.

class BankAccount {
    balance: int
    invariant self.balance >= 0

    fn withdraw(mut self, amount: int)
        requires amount > 0
        requires self.balance >= amount
    {
        self.balance = self.balance - amount    // proven: invariant preserved
    }
}

Concurrency with spawn and tasks. spawn runs a function on a new thread and returns a Task<T>. Error handling composes naturally – errors from spawned functions flow through .get() and are caught the same way as any other error.

let t1 = spawn compute_prices(catalog)
let t2 = spawn fetch_inventory(warehouse)
let prices = t1.get()!
let stock = t2.get()!

Values and entities. class declares a value: structural ==, deep-copied across spawn. object declares an entity: reference identity, shared across spawn with per-instance serialized methods, crossing placement boundaries as an identity handle rather than a copy. The distinction most languages leave as convention is a declaration the compiler enforces.

object Counter {
    value: int
    fn increment(mut self) { self.value = self.value + 1 }
}

Typestates. A protocol is a type: Lease<Held> and Lease<Idle> are different types, a method can exist only in some states, and transitions consume the old binding so stale aliases are compile errors. States can be marked must_release — dropping the obligation without discharging it does not compile.

AI-native development. Pluto’s compiler exposes a structured API (MCP tools and a programmatic SDK) so AI agents can read, write, and refactor code at the semantic level – declarations, types, cross-references – rather than manipulating raw text.

Why Separate Compilation Fails for Backend Systems

Go, Java, and Rust all use separate compilation. They compile each package or crate independently, then link them together. This is great for build times and incremental compilation, but it means the compiler never sees your complete program.

The result? All the cross-cutting backend concerns get pushed to runtime:

• Dependency injection becomes a runtime container (Spring) or a code generation tool run as a separate build step (wire). The container uses reflection to discover services at startup. Errors happen at runtime, not compile time.

• Error handling becomes conventions. Go returns (T, error) tuples and you write if err != nil at every call site — but the compiler doesn’t enforce it. Java has checked exceptions, but you annotate every function signature manually with throws. Rust has Result<T, E>, but you choose between .unwrap() (crash) and .expect() (crash with message) or explicit match.

• Service communication becomes frameworks. You add @RestController annotations and a framework scans them at startup, builds routing tables via reflection, and handles serialization with more reflection. Or you write explicit HTTP client code, manual JSON marshaling, and duplicate error handling logic.

The common thread: the compiler doesn’t know what you’re building, so it can’t help you build it correctly.

Pluto’s whole-program compilation makes the compiler your infrastructure. It knows your dependency graph. It knows your error propagation. It will know your service boundaries. And it generates code accordingly — no runtime, no reflection, no surprises.

Implemented vs. Designed

Pluto is transparent about its maturity. The following features are implemented and working today:

• Dependency injection (bracket deps and ambient deps), compile-time wired
• Error handling with compiler-inferred fallibility, enforced handling, and proof-based error-set shrinking at call sites
• The app construct with synthetic main generation
• Contracts: invariants proven at compile time (strict), including two-state relations via old(); proof-form ensures postconditions assumed by callers; guarded_by write-fencing dominance proofs; requires runtime-checked at entry; assert as prover input
• Objects (entities): identity ==, spawn-sharing with per-instance serialized methods, generic objects, identity handles across boundaries
• Typestates: where S == State method gating, transition linearity, must_release states, degradation errors carrying post-failure state
• Concurrency via spawn, Task<T> (must-use, detach, cancel), channels, copy-on-spawn, and inferred synchronization for DI singletons
• Distribution: at placement over domain dependencies, serve, stage declarations, system compilation (one binary per member), schema-level wire format, interface hashing, definite/ambiguous boundary-failure classification (NetworkError.definite)
• Nullable types (T?, none, ? propagation) and flow narrowing
• Modules, packages, and visibility (pub)
• Generics (monomorphized)
• Test framework (test "name" { ... } with expect assertions)
• Standard library: base64, collections, env, fs, http, io, json, log, math, net, path, random, regex, rpc, socket, strings, time, uuid, wire

Still direction, not implementation: the deployment-plan artifact that binds domains to physical placement, deadline/cancellation propagation across boundaries, cross-entity invariants, and the property form that lets libraries name and export proof bundles like idempotent — see the Vision chapters.

The language is real, compiles to real binaries, and runs real programs. The unimplemented features represent the roadmap, not the reality.

How to read this book

This book is written for experienced developers. It does not explain what a variable is or how a for loop works. It explains what Pluto does differently and why.

Part 1 (Getting Started) gets you running code. Part 2 (What Sets Pluto Apart) covers the features that justify a new language. Part 3 (The Language) is the reference for syntax, types, and standard library. Part 4 (The Vision) covers where the language is headed: AI-native development and verified distribution.

See Chapter 2 for a complete working example.

Installation

Pluto is currently installed from source.

Prerequisites

• Rust toolchain (stable): https://rustup.rs
• C toolchain for linking generated binaries (clang or gcc)

Building from source

git clone https://github.com/Mkerian10/pluto.git
cd pluto
cargo build --release

The compiler binary will be at target/release/pluto.

Optional: Install to PATH

cargo install --path .

Then verify installation:

pluto --help

A Taste of Pluto

This chapter walks through a complete Pluto program — an order-processing service with dependency injection, error handling, and an app entry point. Pay attention to what you don’t write: no manual wiring in main(), no error annotations on functions, no @Inject decorators, no framework initialization. The compiler handles it by seeing your entire program at compile time.

The goal is to show how Pluto’s features work together in practice, not to explain every detail. Subsequent chapters cover each construct in depth.

The program

error OrderError {
    reason: string
}

class OrderValidator {
    fn validate(self, amount: int) {
        if amount <= 0 {
            raise OrderError { reason: "amount must be positive" }
        }
    }
}

class OrderService[validator: OrderValidator] {
    processed: int

    fn process(self, id: string, amount: int) string {
        self.validator.validate(amount)!
        return f"Order {id} processed for {amount}"
    }
}

app OrderSystem[svc: OrderService] {
    fn main(self) {
        let result = self.svc.process("ORD-1", 100) catch err {
            print("Failed: order rejected")
            return
        }
        print(result)
    }
}

Save this as main.pt and run it:

$ pluto run main.pt
Order ORD-1 processed for 100

That is a complete, runnable program. No main function signature to memorize, no framework to initialize, no dependency container to configure. The compiler handles all of it.

Breaking it down

Error declaration. error OrderError defines a typed error with a reason field. Errors in Pluto are not exceptions, not sum types, and not integer codes. They are their own language concept – declared at the top level, raised explicitly, and tracked by the compiler through the entire call graph.

error OrderError {
    reason: string
}

Classes and methods. OrderValidator is a class with a method. Nothing surprising here – but notice that validate does not declare that it can raise an error. The compiler infers this from the raise statement inside the body. You never annotate fallibility.

class OrderValidator {
    fn validate(self, amount: int) {
        if amount <= 0 {
            raise OrderError { reason: "amount must be positive" }
        }
    }
}

Bracket dependencies. OrderService[validator: OrderValidator] declares that OrderService depends on an OrderValidator. The compiler will create the validator, create the service, and inject the dependency – all at compile time. There is no runtime container, no reflection, no @Inject annotation. The validator field is available on self like any other field.

class OrderService[validator: OrderValidator] {
    processed: int

    fn process(self, id: string, amount: int) string {
        self.validator.validate(amount)!
        return f"Order {id} processed for {amount}"
    }
}

Error propagation with !. The ! after self.validator.validate(amount) means: if this call raises an error, propagate it to my caller. The compiler knows that validate can raise OrderError (it inferred this), and it knows that process now can too (it inferred this as well). The ! is the only annotation you write, and it is an explicit decision to propagate rather than handle.

String interpolation. f"Order {id} processed for {amount}" embeds expressions directly in the string. Any expression works inside the braces — but only in f-strings. A plain "{id}" is literal text; interpolation requires the f prefix.

The app declaration. app OrderSystem[svc: OrderService] is the root of the program. It declares its dependencies in brackets, just like a class. The compiler builds the full dependency graph – OrderSystem needs OrderService, which needs OrderValidator – performs a topological sort, allocates everything, wires it together, and calls main.

app OrderSystem[svc: OrderService] {
    fn main(self) {
        let result = self.svc.process("ORD-1", 100) catch err {
            print("Failed: order rejected")
            return
        }
        print(result)
    }
}

Error handling with catch. The catch err { ... } block handles any error raised by process. Inside the block, you can execute arbitrary statements – here we print a message and return from main. If you wrote catch "default" instead, the catch expression would evaluate to the string "default" as a fallback value. Both forms exist because error handling sometimes means recovering with a value and sometimes means bailing out.

The same program in Go

For comparison, here is the equivalent Go program. This is not a contrived strawman – it is what you would actually write.

package main

import "fmt"

type OrderError struct {
    Reason string
}

func (e *OrderError) Error() string {
    return e.Reason
}

type OrderValidator struct{}

func (v *OrderValidator) Validate(amount int) error {
    if amount <= 0 {
        return &OrderError{Reason: "amount must be positive"}
    }
    return nil
}

type OrderService struct {
    Validator *OrderValidator
    Processed int
}

func (s *OrderService) Process(id string, amount int) (string, error) {
    if err := s.Validator.Validate(amount); err != nil {
        return "", err
    }
    return fmt.Sprintf("Order %s processed for %d", id, amount), nil
}

func main() {
    validator := &OrderValidator{}
    svc := &OrderService{
        Validator: validator,
        Processed: 0,
    }

    result, err := svc.Process("ORD-1", 100)
    if err != nil {
        fmt.Printf("Failed: order rejected\n")
        return
    }
    fmt.Println(result)
}

The Go version is roughly twice as long, and the additional lines are not doing interesting work. They are: implementing the error interface, returning tuples, writing if err != nil, and manually constructing and wiring dependencies in main. Every Go backend team writes this scaffolding, and every team writes it slightly differently.

In Pluto, these decisions are made once — in the language — and enforced by the compiler. The error interface is replaced by a typed error declaration. The tuple return is replaced by compiler-tracked fallibility. The if err != nil is replaced by ! and catch. The manual wiring in main is replaced by bracket dependencies and the app construct.

What the Compiler Generated

The Pluto program above compiles to a self-contained native binary. Here’s what the compiler generated behind the scenes:

Dependency graph resolution: The compiler saw that OrderSystem depends on OrderService, which depends on OrderValidator. It performed a topological sort: OrderValidator first, then OrderService, then OrderSystem. It generated a synthetic main() function that allocates them in order and wires the dependencies:

// Generated C-like pseudocode (actual output is Cranelift IR)
int main() {
    OrderValidator *validator = calloc(1, sizeof(OrderValidator));
    OrderService *svc = calloc(1, sizeof(OrderService));
    svc->validator = validator;  // wire the dependency
    svc->processed = 0;
    OrderSystem *app = calloc(1, sizeof(OrderSystem));
    app->svc = svc;  // wire the dependency
    OrderSystem_main(app);  // call app.main(self)
    return 0;
}

No container. No reflection. No service locator. Just allocation and wiring, all resolved at compile time.

Error set inference: The compiler walked the call graph:

• OrderValidator.validate contains raise OrderError → inferred as fallible, error set = {OrderError}
• OrderService.process calls validate! → propagates errors → inferred as fallible, error set = {OrderError}
• OrderSystem.main calls process with catch → handles errors → inferred as non-fallible

The compiler enforced that every fallible call site has either ! (propagate) or catch (handle). If you removed the ! from the validate call, compilation would fail with: error: call to fallible method 'validate' must be handled with ! or catch.

Dead code elimination: If you added a BillingService class but never referenced it in OrderSystem’s dependencies, it wouldn’t be in the final binary. The compiler only allocates and wires what you actually use.

This is what whole-program compilation gives you: the compiler sees everything, understands the structure of your program, and generates exactly the code you need.

What Comes Next

The chapters in Part 2 cover each of Pluto’s distinguishing features in detail: error handling, dependency injection, the app model, concurrency, and contracts. If you need a quick refresher on variables, functions, or control flow, see Chapter 8: Syntax at a Glance.

Whole-Program Compilation

The foundational difference between Pluto and other backend languages is this: Pluto sees your entire program at compile time.

Go compiles each package separately. Java compiles each class separately. Rust compiles each crate separately. They link the pieces together later, but the compiler never sees the complete picture. It sees isolated functions, isolated modules, isolated libraries.

Pluto’s compiler sees all of it: every function, every class, every call site, every error that could be raised, every dependency relationship. It builds a complete call graph, traces error propagation across the entire program, resolves all type parameters, and generates a self-contained native binary with all the wiring baked in.

This is called whole-program compilation, and it’s the reason Pluto can do things that would be impossible — or require runtime magic — in other languages.

What the Compiler Sees

When you compile a Pluto program, the compiler builds:

The complete call graph. Every function call in your program, resolved to a specific function. Not a virtual dispatch table, not a runtime lookup — the compiler knows exactly which function is called at every call site.

The dependency graph. Every class that depends on another class, traced through bracket dependencies. The compiler performs a topological sort and knows the exact allocation order for every singleton in your program.

The error propagation graph. Every function that can raise an error, every call site that propagates errors with !, every catch block that handles errors. The compiler computes the exact error set each function can produce and enforces handling at every call site.

The complete type instantiation set. Every generic type or function instantiated with concrete type arguments. If you use Box<int> and Box<string>, the compiler generates exactly those two concrete versions. If you never use Box<float>, it doesn’t exist in your binary.

The module structure. Every import, every pub declaration, every cross-module reference. The compiler knows which code is reachable from your app.main() and which code is dead.

This isn’t runtime analysis. This isn’t profiling. This is compile-time, whole-program understanding.

What It Gives You

Zero-Cost Dependency Injection

Because the compiler sees the complete dependency graph, it can generate explicit allocation and wiring code. At runtime, there is no container, no reflection, no service discovery — just a sequence of calloc calls in dependency order.

app API[users: UserService, db: Database] {
    fn main(self) { ... }
}

The compiler sees that API depends on UserService and Database. It sees that UserService might also depend on Database. It builds the full graph, topologically sorts it, and generates:

Database *db = calloc(1, sizeof(Database));
UserService *users = calloc(1, sizeof(UserService));
users->db = db;  // wire the dependency
API *app = calloc(1, sizeof(API));
app->users = users;
app->db = db;
API_main(app);

This is literally what the compiler generates (the actual output is Cranelift IR, but the concept is the same). No container. No reflection. No runtime cost. The dependency graph is resolved at compile time.

Compiler-Inferred Error Handling

Because the compiler sees the complete call graph, it can trace error propagation across every function call and compute the exact error set for each function.

fn find_user(id: int) User {
    if id <= 0 { raise NotFound { id: id } }
    return query_db(id)!  // might raise DatabaseError
}

The compiler walks the call graph:

• find_user contains raise NotFound → add NotFound to its error set
• find_user calls query_db! → propagate DatabaseError to its error set
• Final error set for find_user: {NotFound, DatabaseError}

Every caller of find_user must use ! or catch. If you forget, compilation fails:

fn process(id: int) {
    let user = find_user(id)  // ERROR: unhandled fallible call
}

This analysis only works because the compiler sees the whole program. With separate compilation, you’d have to annotate every function signature manually (throws NotFound, DatabaseError). Pluto infers it.

Dead Code Elimination

Because the compiler sees every call site, it knows what’s reachable from main() and what’s not.

fn used() { print("called") }
fn unused() { print("never called") }

fn main() { used() }

The compiler sees that unused is never called from main() or any function reachable from main(). It doesn’t generate code for it. The final binary contains used and main, but not unused.

This extends to classes, imports, and generics. If you import a module but don’t use any of its pub functions, they don’t exist in your binary. If you declare a generic class but never instantiate it, it doesn’t exist in your binary.

Monomorphization of Generics

Because the compiler sees every instantiation of every generic type, it knows exactly which concrete versions to generate.

class Box<T> {
    value: T
}

fn main() {
    let b1 = Box<int> { value: 42 }
    let b2 = Box<string> { value: "hello" }
}

The compiler sees two instantiations: Box<int> and Box<string>. It generates two concrete classes:

struct Box__int { int64_t value; };
struct Box__string { void *value; };

If you never instantiate Box<float>, it doesn’t exist. No vtables, no type erasure, no runtime type checking. The type parameters are resolved at compile time.

Future: Cross-Service RPC Generation

This is the big one. Because the compiler will see the complete call graph, it will know which function calls cross service boundaries.

// service A
fn process_order(order: Order) Receipt {
    let payment = payment_service.charge(order)!  // crosses service boundary
    return generate_receipt(payment)
}

The compiler will see that payment_service.charge is declared in service B. It will generate serialization code for Order, HTTP client code for the call, deserialization code for Receipt, and automatic error propagation for network failures.

You write function calls. The compiler generates RPC. This is only possible with whole-program analysis.

The Trade-Off

Whole-program compilation has a cost: build times. The compiler must see your entire program every time you compile. For small programs, this is fine. For large programs, this can be slow.

Pluto mitigates this with incremental compilation: the compiler caches type-checked modules and only recompiles what changed. But the final link step — resolving the dependency graph, computing error sets, generating the synthetic main — requires seeing the whole program.

This is the trade-off: longer build times in exchange for zero-cost abstractions, compiler-enforced correctness, and the ability to solve cross-cutting concerns at compile time rather than runtime.

For backend services, where deployment frequency is measured in hours or days, and where runtime performance and correctness matter more than local iteration speed, this is the right trade-off.

Why Other Languages Don’t Do This

The short answer: backwards compatibility and build times.

C and C++ have separate compilation because build times for large programs would be unbearable otherwise. They use link-time optimization (LTO) to recover some whole-program visibility, but LTO is slow and optional.

Go has separate compilation because it prioritizes fast incremental builds. The Go toolchain is famously fast, but it means the compiler can’t do whole-program analysis. Dependency injection becomes manual wiring or wire (a separate code generation tool). Error handling becomes conventions (if err != nil).

Java has separate compilation because the JVM needs to support loading classes at runtime. It can’t see the whole program because the program isn’t fully known until runtime. Dependency injection becomes Spring (a runtime container with reflection). Error handling becomes checked exceptions (manual annotations).

Rust has separate compilation because incremental builds are a priority for developer ergonomics. It uses monomorphization like Pluto, but only within a crate. Cross-crate generics use trait objects (dynamic dispatch) unless you enable LTO.

Pluto starts from a different constraint: backend services, where correctness and runtime performance matter more than local build speed. The trade-off makes sense for this domain.

Summary

Whole-program compilation is not free. It costs build time. But it gives you:

• Zero-cost dependency injection (no container, no reflection)
• Compiler-inferred error handling (no manual annotations)
• Dead code elimination (only what you use)
• Monomorphized generics (no vtables, no boxing)
• Future: RPC generation from function calls

All of Pluto’s distinguishing features — DI, error inference, the app model, contracts — are built on this foundation. The compiler sees your entire program, understands its structure, and generates exactly the code you need.

This is what justifies a new language.

Source-Level Libraries — No Boundaries

Pluto has libraries. You can write them, publish them, depend on them, and import them into your programs. But they work fundamentally differently than libraries in other languages.

Traditional libraries are compiled separately into binary artifacts (.so, .dll, .jar, .rlib). The compiler sees an opaque interface. The library is a black box.

Pluto libraries are always source code. When you depend on a package, the compiler pulls in the source and sees everything: every function, every type, every implementation detail (that’s marked pub or used by your code).

There is no binary artifact. There is no ABI boundary. There is no separate compilation. The compiler always sees the source.

This isn’t about whether libraries exist. It’s about how they’re compiled. In Rust, you compile a crate to an .rlib, and consumers link against it. In Go, you compile a package to a .a archive. In Java, you compile to a .jar. The consumer never sees your source code — only the binary interface.

In Pluto, when you depend on a library, you depend on source code. The Pluto compiler pulls that source into your build and sees everything. It can inline functions across library boundaries. It can eliminate dead code from the library. It can specialize generic types based on how you use them. The library isn’t a black box — the compiler sees through it.

Why Other Languages Have Binary Libraries

The library/executable split exists for three reasons:

1. Build times. If you had to recompile all your dependencies every time you changed one line, builds would be unbearably slow. Separate compilation means you compile each library once, emit a binary artifact, and reuse it across builds.

2. Distribution. If you want to share code without sharing source, you need a binary format. C libraries ship as .so or .dll files. Rust crates compile to .rlib files. The consumer links against the binary without seeing the original source.

3. ABI stability. Once you ship a binary library, you can’t change its interface without breaking everyone who depends on it. The ABI (Application Binary Interface) is a contract: “here’s how to call my functions in machine code.” This enables separate compilation and dynamic linking, but it also locks you into your decisions.

The result: compilers can’t see across library boundaries. They can’t inline functions from dependencies. They can’t eliminate dead code from libraries. They can’t specialize generics based on how you use them. The library is opaque.

Pluto’s Model: Everything is Source

In Pluto, there are no binary artifacts. When you depend on a package, you depend on source code. The compiler pulls that source into your program and sees everything.

# pluto.toml
[dependencies]
http = { git = "https://github.com/pluto-lang/http", tag = "v1.0" }
db = { path = "../shared/database" }

When you compile your program, the compiler:

1. Fetches the source for http and db
2. Parses them
3. Flattens them into your program’s namespace
4. Type-checks the whole thing together
5. Performs whole-program optimizations
6. Generates a single native binary

The http package isn’t a black box. The compiler sees every function in it. If you only call http.get and never use http.post, the compiler doesn’t generate code for post. If http.parse_headers is only called once and it’s small, the compiler inlines it. If you instantiate http.Client<MyConfig>, the compiler generates a specialized version of the client for your config type.

This is only possible because the compiler sees the source.

No ABI Means No Breakage

Because there’s no binary artifact, there’s no ABI to break. If you update a dependency, the compiler re-analyzes the whole program. If the types changed incompatibly, you get a compile error. If the error sets changed, you get a compile error. If a function you called was removed, you get a compile error.

There’s no such thing as “runtime dependency resolution failure.” There’s no LD_LIBRARY_PATH to configure. There’s no version of a library loaded at runtime that’s incompatible with what you compiled against. If it compiles, the dependencies are correct.

How Pluto Libraries Work

A Pluto library (or package) is a collection of source files with pub declarations. It’s not a compiled artifact. It’s not a binary. It’s source code that the compiler integrates into your program.

// In package "payments"
pub fn charge(amount: int) Receipt {
    return process_transaction(amount)!
}

fn process_transaction(amount: int) Receipt {
    // internal implementation
}

When you import this library, the compiler sees both functions — charge (public) and process_transaction (internal). It knows that process_transaction is only called from within the payments library. If it’s small, it might inline it into charge. If it’s never called, it won’t generate code for it.

The consumer sees:

import payments

fn main() {
    let receipt = payments.charge(100)!
}

The compiler knows that charge can fail (it contains !), infers the error set, and enforces handling. It knows the return type is Receipt. It knows whether Receipt has any fields you’re accessing. It sees everything.

Apps, Not Executables

The unit you compile is not an “executable.” It’s an app. The app is a first-class language construct:

app PaymentService[db: Database, cache: Cache] {
    fn main(self) {
        // entry point
    }
}

The compiler generates a native binary for this app. The binary is self-contained: all dependencies are compiled in, all wiring is done, all error handling is checked. There’s no external configuration file that changes the dependency graph. There’s no classpath. There’s no dynamic linking. It’s a single binary that does one thing.

Source-Level Composition Extends Across Services

The same principle scales past one process. A system declaration composes multiple modules into a distributed application, and because every member is source, the compiler checks them against each other: an orders service’s dependency on a billing interface is verified against the billing service that actually serves it — types, error contracts, interface hashes — before either binary is built. Placement expressions (at domain { ... }) carry computation across boundaries with the transport synthesized from the deployment binding, not written by hand.

This is the opposite of libraries. Libraries hide details from the compiler. Source-level composition exposes details to the compiler so it can generate and check cross-service communication. See the Distribution chapter for the full model.

No Dynamic Linking, Ever

Pluto will never support dynamic linking. It will never have .so files or .dll files. It will never load code at runtime that wasn’t seen at compile time.

This is a deliberate trade-off:

• Pro: The compiler can do aggressive whole-program optimizations. Dead code elimination. Inlining across module boundaries. Monomorphization of generics. Static analysis of error propagation.
• Con: You can’t ship a “Pluto library” as a binary artifact. You can only share source.

For backend services, this is the right trade-off. Backend services aren’t plugins. They’re not loaded dynamically. They’re deployed as containers or binaries, and they do one thing. Pluto optimizes for that use case.

The Package Ecosystem

When Pluto has a package registry, it won’t be like npm or crates.io where packages are versioned binaries. It will be a registry of source repositories with tagged versions.

Publishing a package means:

1. Tag a commit in your git repo
2. Register the repo + tag with the registry
3. Document the pub API surface

Depending on a package means:

1. The compiler fetches the source at the specified tag
2. The compiler parses and type-checks it
3. The compiler integrates it into your program

There’s no “build the package, upload the artifact, download the artifact, link against it” step. The compiler always works with source.

Binary AST as an Optimization

(This section is aspirational — the binary AST format exists but isn’t the default yet.)

Eventually, Pluto will support a binary AST format (.pluto files) as an optimization for large codebases. This isn’t a binary library in the traditional sense — it’s a serialized parse tree with type information.

When you compile a program, the compiler can cache the parsed and type-checked AST for each module. On the next build, if a module hasn’t changed, the compiler reuses the cached AST instead of re-parsing the source.

But the key difference from traditional libraries: the compiler still sees the AST. It can still inline functions, eliminate dead code, specialize generics. The binary AST is an optimization for build times, not an ABI boundary.

The workflow:

1. Write .pt source files (Pluto text format)
2. Compiler parses them into .pluto binary AST
3. Compiler caches the .pluto files
4. On incremental builds, compiler reuses cached .pluto files for unchanged modules
5. Final whole-program analysis and codegen happens across all modules, cached or not

You never ship a .pluto file to users as a “library.” You always share source. The binary AST is a local build cache.

What This Means for You

If you’re coming from Go, Java, or Rust, this is a mental shift:

You DO write libraries. But you write them as collections of .pluto source files with pub declarations. You don’t compile them into standalone binary artifacts.

You don’t link binaries. The compiler generates one self-contained binary for your app. All dependencies are compiled in (from source). There’s no runtime linker, no LD_LIBRARY_PATH, no classpath.

You don’t publish binary artifacts. If you want to share a library, you publish source code (via git repos or a future package registry). The consumer’s compiler pulls your source and integrates it into their program.

You don’t version ABIs. There’s no ABI because there’s no binary artifact. If you change your library’s pub API, consumers recompile and get immediate feedback if the change broke them. Semantic versioning still matters (breaking changes vs. non-breaking changes), but there’s no “runtime version mismatch” or “DLL hell.”

The benefit: the compiler always sees your entire program, from main() to the deepest dependency, and can optimize accordingly. Libraries aren’t black boxes. They’re transparent to the compiler.

The Vision

The endgame for Pluto is a programming model where:

• You write source. Functions, classes, errors, contracts.
• You declare dependencies. Packages from git repos, local paths, or a future registry.
• You define stages. Independently deployable units within your program.
• The compiler sees everything. Every function, every call site, every error, every dependency, every stage boundary.
• The compiler generates deployment artifacts. One binary per stage, with all RPC, serialization, and error handling generated automatically.

No libraries. No dynamic linking. No reflection. No runtime containers. No frameworks discovering your code at startup.

Just source code, whole-program analysis, and native binaries that do exactly what you wrote.

This is what justifies rejecting the library/executable distinction. The compiler becomes your infrastructure.

Error Handling

Every language gets error handling wrong in its own special way.

Go chose explicit returns: val, err := doThing(). The intent was good – errors are values, not magic. But the result is if err != nil on every third line, an entire codebase of boilerplate that teaches developers to stop reading error paths. Worse, nothing stops you from ignoring the err return entirely.

Java chose checked exceptions. In theory, the signature tells you what can fail. In practice, developers wrap everything in RuntimeException to escape the type system, and throws Exception becomes the universal surrender flag. The community collectively decided checked exceptions were a mistake.

Rust chose Result<T, E>. It is correct. It is also verbose. map_err, From implementations, custom error enums with thiserror, the ? operator threading through six layers of adapters – Rust’s error handling is powerful enough to model anything and ergonomic enough to model nothing without a crate.

JavaScript chose to pretend errors do not exist. try-catch is optional, async functions silently swallow unhandled rejections, and Promise chains lose context by default. The developer is on their own.

Pluto takes a different path.

Errors Are a Language Concept

Pluto errors are not exceptions. There is no stack unwinding. There is no hidden control flow. There is no performance penalty for code that does not raise.

Pluto errors are not sum types. You do not write Result<User, NotFoundError | PermissionError> and pattern match on variants.

Errors in Pluto are their own thing: declared types, raised explicitly, inferred by the compiler, and enforced at every call site.

Declaring Errors

An error is declared with the error keyword. It is a lightweight struct:

error NotFound {
    id: int
}

error ValidationError {
    field: string
    message: string
}

error Timeout {}

Errors can have fields (for context) or be empty (when the type name says enough).

Raising Errors

The raise keyword creates and throws an error:

fn find_user(id: int) User {
    if id < 0 {
        raise NotFound { id: id }
    }
    return lookup(id)
}

After a raise, execution leaves the function immediately. No error is “returned” – it is set in a side channel and the caller is responsible for checking it.

The Compiler Infers Error-Ability

Here is the key difference from every other language: you do not annotate functions with error information. The compiler figures it out.

fn step1() int {
    raise Timeout {}
    return 0
}

fn step2() int {
    let x = step1()!
    return x + 1
}

fn step3() int {
    let x = step2()!
    return x + 1
}

The compiler walks the entire call graph: step1 is fallible (contains raise), step2 is fallible (propagates from step1 via !), step3 is fallible (propagates from step2).

No throws keyword. No Result return type. No error type parameter. The compiler does a fixed-point analysis across the whole program and knows exactly which functions can fail, transitively.

This means you never have to update function signatures when error-ability changes deep in a call chain. If step1 stops raising, the compiler re-infers the entire graph and step2 and step3 become infallible automatically.

Propagation with !

The ! postfix operator propagates an error to the caller:

fn process(id: int) int {
    let user = find_user(id)!    // if find_user raises, propagate to our caller
    return user.age
}

This is similar to Rust’s ?, but there is no Result to unwrap. The ! checks the error channel, and if an error was raised, it immediately returns from the current function, forwarding the error.

The compiler enforces that ! is only used on fallible calls. Using ! on an infallible function is a compile error:

fn safe() int { return 42 }

fn main() {
    let x = safe()!    // COMPILE ERROR: safe() is infallible
}

Handling Errors with catch

The catch keyword handles errors at the call site. There are three forms.

Shorthand catch provides a default value:

let result = find_user(-1) catch default_user
let port = parse_port(input) catch 8080

If the call raises any error, the expression evaluates to the value after catch. The type must match.

Wildcard catch binds the error and runs a block:

let result = find_user(-1) catch err {
    log("User lookup failed")
    return
}

The block can contain multiple statements. If it does not return or exit, its final expression becomes the value:

let result = find_user(-1) catch err {
    let fallback = 42
    fallback
}

Typed catch handles specific error types, with coverage checking. Chain typed handlers, and finish with a wildcard (or !) for anything not named:

error NotFound {
    id: int
}

error Timeout {}

fn lookup(id: int) int {
    if id < 0 {
        raise NotFound { id: id }
    }
    if id > 1000 {
        raise Timeout {}
    }
    return id * 2
}

fn main() {
    let v = lookup(-1) catch err: NotFound {
        print(f"missing id {err.id}")
        0
    } catch err {
        -1
    }
    print(v)
}

Inside a typed handler, the error binding has that error’s type — its fields are directly accessible. The compiler checks coverage against the call’s error set: name every variant and no wildcard is needed; leave one unnamed without a fallback and compilation fails.

The Compiler Enforces Handling

This is the part that matters most. In Pluto, you cannot call a fallible function without handling the error. It is a compile error:

fn main() {
    find_user(-1)    // COMPILE ERROR: fallible call must be handled with ! or catch
}

There is no way to accidentally ignore an error. There is no way to “forget” to check. The compiler rejects the program.

Similarly, you cannot use catch or ! on infallible functions – the compiler rejects unnecessary error handling to keep code honest:

fn safe() int { return 42 }

fn main() {
    let x = safe() catch 0    // COMPILE ERROR: safe() is infallible
}

Proofs Shrink Error Sets

Error inference is not just per-function — it is sensitive to what the compiler can prove at each call site. If your guard makes a callee’s raise impossible, the handling obligation disappears at that site:

error Insufficient {
    needed: int
}

class Account {
    balance: int

    fn withdraw(mut self, amt: int)
        requires amt > 0
    {
        if amt > self.balance {
            raise Insufficient { needed: amt }
        }
        self.balance = self.balance - amt
    }
}

fn main() {
    let mut account = Account { balance: 100 }
    let amt = 30
    if amt <= account.balance {
        account.withdraw(amt)        // no ! — Insufficient is proven impossible here
        print(account.balance)       // 70
    }
}

withdraw is fallible — but at this call site, the caller’s guard (amt <= account.balance) refutes the raise’s condition (amt > self.balance), so Insufficient vanishes from the site’s required-handling set. The same call without the guard is the usual compile error:

account.withdraw(30)
// COMPILE ERROR: call to fallible method 'withdraw' must be handled with ! or catch

Contracts stop being documentation and start removing handling obligations: facts flow in through guards and requires, and the visible payoff is code that gets simpler as it gets more proven.

What shrinks. The shipped analysis is deliberately conservative — soundness is absolute, because a wrongly-dropped variant would be an unhandled runtime error. A variant shrinks only when:

• the raise is direct in the callee’s body, with a dominating guard over the callee’s parameters and the receiver’s direct int fields, still holding their entry values when the guard is evaluated (a raise inside a loop qualifies too, if its guard is loop-invariant — nothing in the loop body disturbs the guarded paths);
• the call is direct — a named function or a method resolved on a concrete class, including generic ones.

Generic callees shrink via the template: a generic function’s guard chains are syntactic and hold verbatim for every instantiation, so one summary serves all of them — provided no guard mentions a type-parameter-dependent field or parameter. That proviso is what admits the typestate pattern, whose state parameters are phantom and whose guards are over plain int fields:

error Degraded {
    code: int
}

class Held {
    tag: int
}

class Lease<S> {
    id: int
    epoch: int

    fn renew(self) Lease<Held> where S == Held {
        if self.epoch > 2 {
            raise Degraded { code: self.epoch }
        }
        return Lease<Held> { id: self.id, epoch: self.epoch + 1 }
    }
}

fn main() {
    let h = Lease<Held> { id: 7, epoch: 1 }
    if h.epoch <= 2 {
        let h2 = h.renew()      // no ! — Degraded is proven impossible here
        print(h2.epoch)         // 2
    }
}

renew is a where-constrained transition on a generic class, and it still shrinks: the caller’s fact on h.epoch refutes the raise condition, so the transition needs no handler exactly where the lease is provably fresh. Typestates and error shrinking compose — the protocol keeps its state machine and its call sites get simpler.

What never shrinks. Variants that arrive via propagation (! edges), closures, fn-typed values, trait dispatch, channel operations, and remote boundaries are untouched, and a generic caller never shrinks its own sites. And the caller’s facts must still be alive at the call: a reassignment, a field write, or an interleaved call that could mutate the receiver kills the guard, and the obligation comes back —

if amt <= account.balance {
    account.withdraw(90) catch err {   // this call may change balance...
        print(0)
    }
    account.withdraw(amt)              // COMPILE ERROR: guard no longer trusted
}

Shrinking narrows individual call sites only. The callee’s canonical error set — and therefore what ! propagates — never changes, and handling a provably-impossible error stays legal: a catch on a shrunk-to-empty site still compiles, so defensive handlers survive refactors that make them unnecessary.

Method Error Handling

Error handling works identically on method calls:

error ConnectionFailed {
    reason: string
}

class Database {
    _host: string

    fn query(self, sql: string) string {
        if self._host == "" {
            raise ConnectionFailed { reason: "no host" }
        }
        return "result"
    }
}

fn main() {
    let db = Database { _host: "localhost" }
    let result = db.query("SELECT 1") catch "fallback"
    print(result)
}

The compiler infers method fallibility the same way it infers function fallibility. If any implementation of a trait method is fallible, the trait dispatch is considered fallible:

trait Worker {
    fn work(self) int
}

class Risky impl Worker {
    fn work(self) int {
        raise Fail {}
        return 0
    }
}

fn use_worker(w: Worker) int {
    return w.work()    // COMPILE ERROR: must be handled
}

Errors and Concurrency

When you spawn a function that can raise, the error flows through the task handle’s .get() call:

error MathError {
    message: string
}

fn divide(a: int, b: int) int {
    if b == 0 {
        raise MathError { message: "division by zero" }
    }
    return a / b
}

fn main() {
    let task = spawn divide(10, 0)
    let result = task.get() catch -1    // error surfaces here
    print(result)
}

The compiler knows that .get() on a task wrapping a fallible function is itself fallible. You must handle it with ! or catch – the same rules apply.

Errors at a Distance: NetworkError.definite

When a call crosses a process boundary — a remote dependency, an at placement bound to another process — the compiler adds NetworkError to the call’s inferred error set, and handling it is mandatory like any other variant. NetworkError carries two fields: message, the human-readable cause, and definite, the one bit that actually governs what you may do next.

Every failed boundary call is one of exactly two kinds:

• Definite (definite == true) — the request is known not to have been dispatched: no address bound, connection refused, the request frame never completed, or the server itself replied that it refused to dispatch (unknown method, interface-hash mismatch). The world is in a known state. You may react freely — including retrying a non-idempotent call, because the effect did not happen.
• Ambiguous (definite == false) — the request left the process and no response came back. The effect applied, or it didn’t; no local information can tell you which. A blind retry of a non-idempotent effect here is the classic double-charge bug. The legitimate exits are the careful ones: retry only through an idempotency key, read the state back, fence the old attempt out, or escalate honestly.

import billing

app Payments[billing: remote billing.BillingService] {
    fn main(self) {
        let x = self.billing.charge(21) catch err: NetworkError {
            if err.definite {
                // The request was never dispatched. The world is in a known
                // state — react freely, including retrying a non-idempotent call.
                print("charge did not happen; safe to retry")
            } else {
                // The request left and nothing came back. The charge may or
                // may not exist. Do NOT blind-retry a non-idempotent effect.
                print("charge outcome unknown; reconcile before retrying")
            }
            return
        }
        print(f"charged: {x}")
    }
}

The classification is drawn by the runtime — the only layer that knows whether the bytes left the socket — and it is truthful by construction: definite == true is only ever set with a warrant (the connection never opened; the length-framed request was never completed, and the server dispatches only on a complete frame; the authority itself reported the refusal). When in doubt, the runtime claims ignorance: the default is ambiguous. There are no hidden transport retries, either — each boundary call dials, sends, and reads exactly once, so retry policy stays with the caller, who is the only party holding the classification.

Two fixes worth knowing rode in with this feature. A typed catch err: NetworkError now matches transport-raised failures — previously they carried no type tag, silently fell through typed handlers, and escaped (only a wildcard catch caught them). And a server refusing to dispatch now says so in its reply instead of closing the connection — converting what the client could only have called ambiguous into a definite rejection, a conversion only the authority has the warrant to make.

Comparison

What This Means in Practice

The error system is designed around one insight: the compiler already knows the call graph. Pluto does whole-program compilation. It can trace every call path, determine which functions can raise, and enforce handling at every site – without the programmer writing a single annotation. The result is the safety of Rust, the ergonomics of Go, and the inference of TypeScript – without the downsides of any of them.

Errors are not exceptions. No stack unwinding. No performance penalty. No invisible control flow. Just typed values, raised explicitly, propagated with !, caught with catch, and enforced by the compiler.

Dependency Injection

In Spring Boot, you annotate a class with @Service, annotate its constructor parameters with @Autowired, register a @Configuration class that returns a @Bean, add @Qualifier when types collide, configure @Scope("request") for per-request state, and pray that the runtime container wires everything correctly on the first try. When it does not, you get a stack trace 200 lines deep pointing at a BeanCreationException that tells you almost nothing.

In Go, you write a main() function that manually constructs every dependency and passes it to the next constructor. It is explicit and honest. It is also 300 lines of boilerplate that nobody reads, and every new service means editing main().

In Node with NestJS, you decorate classes with @Injectable(), register them in modules, and debug circular dependency errors at runtime with console output that says “Nest cannot resolve dependencies of the CatsService.”

Pluto has language-level dependency injection. It is resolved at compile time. There is no container. There is no reflection. There are no annotations. The compiler reads the dependency graph, topologically sorts it, detects errors, and generates the wiring code. If something is wrong, you get a compile error, not a runtime crash.

Bracket Deps: Explicit Dependencies

A class declares its dependencies inside square brackets:

class OrderService[db: Database, auth: AuthService] {
    fn process(self, order_id: int) string {
        let user = self.auth.current_user()!
        return self.db.query(f"SELECT * FROM orders WHERE id = {order_id}")!
    }
}

db and auth are injected fields. You access them through self, just like regular fields. The compiler allocates them before regular fields in memory and wires them automatically at startup.

You cannot construct a class with injected deps manually. This is a compile error:

let svc = OrderService { db: some_db, auth: some_auth }
// COMPILE ERROR: classes with injected dependencies cannot be manually constructed

This is intentional. If you could bypass DI and construct services manually, the compiler could not guarantee the dependency graph is correct.

Ambient Deps: Background Services

Some dependencies are cross-cutting. A Logger is used by almost every class. A Config object is read everywhere. Threading these through bracket deps gets noisy:

// Without ambient deps -- every class needs [logger: Logger]
class OrderService[db: Database, auth: AuthService, logger: Logger] { ... }
class PaymentService[gateway: PaymentGateway, logger: Logger] { ... }
class NotificationService[mailer: Mailer, logger: Logger] { ... }

Ambient deps solve this. A class declares that it uses a type, and accesses it as a bare variable:

class OrderService uses Logger [db: Database, auth: AuthService] {
    fn process(self, order_id: int) string {
        logger.info(f"Processing order {order_id}")
        let user = self.auth.current_user()!
        let result = self.db.query("SELECT 1")!
        logger.info("Order processed")
        return result
    }
}

The variable name is the type name with the first letter lowercased: Logger becomes logger, Config becomes config, RequestCtx becomes requestCtx.

A class can use multiple ambient deps: class OrderService uses Logger, Config [db: Database]. Under the hood, ambient deps are desugared to hidden injected fields before type checking. logger.info(...) becomes self.logger.info(...). The rest of the compiler sees regular field access.

The App Declaration

Every Pluto application has an app declaration. It is the root of the dependency graph:

app MyApp[svc: OrderService] {
    ambient Logger
    ambient Config

    fn main(self) {
        self.svc.process()!
    }
}

The app declares:

• Bracket deps – the top-level services it needs direct access to
• Ambient registrations – which types are available as ambient deps throughout the program
• Methods – including the required fn main(self) entry point

Every type used in a uses clause anywhere in the program must be declared ambient in the app. If you forget, the compiler tells you:

// COMPILE ERROR: 'Logger' is not declared ambient in the app

App methods can also use ambient deps. The app itself has access to everything it registers:

app MyApp[svc: OrderService] {
    ambient Logger

    fn main(self) {
        logger.info("Starting application")
        self.svc.process()!
    }
}

Compile-Time Resolution

When the compiler encounters an app declaration, it:

1. Collects all classes and their bracket deps and ambient deps
2. Builds a dependency graph
3. Topologically sorts the graph
4. Checks for cycles – a cycle is a compile error
5. Checks that every dependency has a provider
6. Generates a synthetic main() that allocates singletons in order, wires them, and calls the app’s main(self)

This happens at compile time. The generated binary has no DI container, no reflection, no service locator. Just a sequence of allocations and pointer assignments, then your code runs.

A missing dependency is a compile error. A cycle is a compile error. An ambiguous type is a compile error. You never discover DI problems in production.

Specific Types for Unambiguity

Dependencies are resolved by exact type. If you have two databases, you use two distinct types:

class OrderService[api_db: APIDatabase, accounts_db: AccountsDatabase] {
    fn process(self) {
        let orders = self.api_db.query("SELECT * FROM orders")!
        let user = self.accounts_db.query("SELECT * FROM users")!
    }
}

No @Qualifier("api"). No named bindings. The type is the identifier. APIDatabase and AccountsDatabase are different types, so there is no ambiguity.

Shared Singletons

By default, every class in the DI graph is a singleton. If ServiceA[db: Database] and ServiceB[db: Database] both depend on Database, they get the same instance – one allocation, shared across the graph. No special annotation needed; singleton is the default lifecycle.

Environment Opacity

The code does not know what environment it runs in. A Database class in development might wrap SQLite. In staging, it wraps Postgres. In production, it wraps a replicated Aurora cluster. The code that depends on Database never changes. The runtime and orchestration layer determine what gets constructed. No if (env == "prod") conditionals, no Spring profiles, no environment variables scattered through business logic.

Config as a Class

Configuration in Pluto is not a special construct. It is a class with fields, methods, and invariants:

class DatabaseConfig {
    host: string
    port: int
    max_connections: int

    invariant self.port > 0
    invariant self.port < 65536
    invariant self.max_connections > 0
    invariant self.host.len() > 0

    fn connection_string(self) string {
        return f"{self.host}:{self.port}"
    }
}

Invariants are checked at construction. If someone provides port: -1, the program aborts immediately – not 20 minutes later when the first request hits the database.

Config participates in DI like any other class:

class Database[config: DatabaseConfig] {
    fn connect(self) string {
        return self.config.connection_string()
    }
}

No @Value("${database.host}"). No config.get("database.host"). No process.env.DATABASE_HOST. A typed field on a class, validated by invariants, injected by the compiler.

Environment Variables

Environment variable access uses the std.env stdlib module:

import std.env

fn main() {
    let host = env.get_or("DATABASE_HOST", "localhost")
    let port = env.get_or("DATABASE_PORT", "5432")
    print(f"Connecting to {host}:{port}")
}

For DI-based applications, wrap environment access in a config class to keep it centralized and testable:

import std.env

class DatabaseConfig {
    host: string
    port: int

    invariant self.port > 0
    invariant self.port < 65536
    invariant self.host.len() > 0
}

Lifecycle Scopes

Not every dependency should live for the entire process. A RequestContext is per-request. A database transaction is per-request. Pluto supports three lifecycles:

Singleton is the default. Scoped and transient are declared on the class:

scoped class RequestCtx {
    request_id: string
    user_id: int
}

transient class UUIDGenerator {
    seed: int
}

class Logger {
    fn info(self, msg: string) {
        print(msg)
    }
}

The compiler infers lifecycle when you do not declare one. The rule: a class’s lifecycle is the shortest-lived lifecycle among its dependencies. If UserService depends on singleton Logger and scoped RequestCtx, it is inferred as scoped.

A singleton class explicitly depending on a scoped class is a compile error – the compiler catches captive dependency bugs that Spring silently allows and .NET only catches at runtime.

Scope Blocks

Scoped instances are created inside scope blocks:

app MyApp {
    fn main(self) {
        scope(RequestCtx { request_id: "abc", user_id: 42 }) |svc: UserService| {
            let user = svc.get_user(1)
            print(user)
        }
    }
}

The scope block takes seeds (struct literals for scoped classes that need external values) and bindings (which scoped instances the body needs). The compiler creates all scoped instances at scope entry, wires their dependencies, runs the body, and then the scoped instances become eligible for garbage collection.

Scoped classes that depend only on other injected deps (no regular fields) are auto-created without needing to be seeds. If UserService[ctx: RequestCtx] has no regular fields, the compiler creates it automatically when the scope provides RequestCtx.

Scopes nest, with inner scopes shadowing outer scopes for the same type. Scoped classes can depend on singletons (wired from the global graph), but singletons cannot depend on scoped classes.

App-Level Lifecycle Overrides

The app can shorten a class’s lifecycle without modifying the class itself:

app MyApp {
    scoped Database
    transient Logger

    fn main(self) {
        scope(RequestCtx { id: "r1" }, Database { url: "pg://db" }) |svc: Service| {
            print(svc.run())
        }
    }
}

Overrides can only shorten: singleton to scoped, singleton to transient, or scoped to transient. Lengthening (transient to singleton) is a compile error – it would violate the lifetime guarantees of the original declaration.

Comparison

What This Means in Practice

DI in Pluto is not a framework feature you opt into. It is a language feature the compiler enforces. The dependency graph is fully visible at compile time: every class, every dependency, every lifecycle, every ambient registration. Missing deps, cycles, scope violations, and captive dependencies are all compile errors.

The generated binary has no container. No reflection. No proxy objects. No classpath scanning. Just a sequence of allocations and pointer assignments generated by the compiler from a graph it fully understands. The code you write looks like normal classes with normal methods. The dependencies arrive automatically, validated and wired before a single line of your code runs.

The App Model

Most languages treat “application” as an afterthought. Your program is a main() function. Maybe you wire up a dependency injection container in the first 50 lines, maybe you don’t. The framework handles lifecycle, or you handle it yourself with ad hoc initialization code. The language has no opinion.

Pluto treats the app as the 0th-class object. The app declaration is a top-level language construct that defines your program’s entry point, its dependency graph, and its lifecycle – all in one place, all verified at compile time.

The app Declaration

app OrderSystem[svc: OrderService, db: Database] {
    ambient Logger

    fn main(self) {
        self.svc.process("ORD-1", 100)!
    }
}

This is a complete Pluto program entry point. The compiler reads it and knows:

• What the program needs. OrderService and Database are bracket deps – singleton services created at startup and wired automatically.
• What is globally available. Logger is an ambient type. Any class that declares uses Logger gets a Logger instance injected without listing it as a bracket dep.
• How the program starts. fn main(self) is the entry point. The compiler generates a synthetic main() that allocates all singletons in dependency order, wires them together, and calls self.main().

Compare this to the equivalent in Spring Boot: a @SpringBootApplication class, component scanning, @Autowired annotations scattered across files, runtime reflection to resolve the graph. In Pluto, the entire DI topology is visible in one declaration and verified at compile time.

The App as DI Root

The app is the root of the dependency injection graph. Its bracket deps are the top-level singletons, and their transitive dependencies form the full graph:

class Database {
    fn query(self, sql: string) string {
        return sql
    }
}

class UserService[db: Database] {
    fn get_user(self, id: string) string {
        return self.db.query(f"SELECT * FROM users WHERE id = {id}")
    }
}

class OrderService[db: Database, users: UserService] {
    fn process(self, order_id: string, amount: int) {
        let user = self.users.get_user("42")
        print(f"Processing order {order_id} for {user}: {amount}")
    }
}

app OrderSystem[svc: OrderService] {
    fn main(self) {
        self.svc.process("ORD-1", 100)
    }
}

The compiler resolves the full graph: OrderSystem needs OrderService, which needs Database and UserService, which needs Database. It topologically sorts the dependencies, detects cycles, and generates startup code that allocates one instance of each class in the correct order. Database is created once and shared between UserService and OrderService – it is a singleton.

App Rules

The constraints are strict by design:

• Exactly one per program. A compilation unit has at most one app declaration. Multiple entry points are a compile error.
• Must have fn main(self). The app must define a main method. This is the program’s entry point after DI wiring completes.
• All deps are singletons. Bracket deps on the app and their transitive dependencies are created once and live for the entire process. (See the section on lifecycle overrides below for how to change this.)
• Cycle detection at compile time. If A depends on B and B depends on A, the compiler rejects it immediately. No runtime BeanCurrentlyInCreationException.
• No manual construction of injected classes. If a class has bracket deps (is DI-managed), you cannot construct it with a struct literal. The compiler owns construction.

Ambient Types

Bracket deps are explicit – you access them through self.dep. Ambient types provide a lighter-weight alternative for cross-cutting concerns:

class Logger {
    fn info(self, msg: string) {
        print(msg)
    }
}

class OrderService uses Logger [db: Database] {
    fn process(self) {
        logger.info("processing order")
        print(self.db.query("SELECT 1"))
    }
}

app MyApp[svc: OrderService] {
    ambient Logger

    fn main(self) {
        self.svc.process()
    }
}

uses Logger on a class means “inject a Logger and let me access it as logger” (type name, first letter lowercased). The ambient Logger declaration in the app registers it as available for uses clauses. Every class that uses Logger shares the same singleton instance.

This is syntactic sugar – the compiler desugars uses into hidden injected fields before type checking. But it eliminates significant boilerplate for types like loggers, config, and metrics that every class needs.

Lifecycle Overrides

By default, every DI-managed class is a singleton. But real systems need per-request state – a request context, a database transaction, a metrics collector scoped to a single operation.

Pluto supports scoped and transient lifecycle annotations on classes:

scoped class RequestCtx {
    request_id: string
}

class Handler[ctx: RequestCtx] {
    fn handle(self) string {
        return f"handling {self.ctx.request_id}"
    }
}

The compiler infers that Handler is also scoped because it depends on a scoped class. A singleton depending on a scoped class is a compile error – the captive dependency problem that Spring silently ignores and .NET catches at runtime.

The app can also override a class’s default lifecycle:

app MyApp {
    scoped ConnectionPool

    fn main(self) {
        // ConnectionPool is now per-scope instead of singleton
    }
}

Overrides can shorten a lifecycle (singleton to scoped) but not lengthen it (scoped to singleton). The compiler enforces this.

Project Kinds

Not every Pluto program needs an app. The compiler supports several project kinds:

A plain program has a fn main() function as its entry point. No DI, no ceremony.

A library is declarations only – functions, classes, traits, enums. Libraries are imported by other programs and cannot have entry points.

A system composes multiple modules into a distributed application, checked as one program and compiled to one binary per member. See the Distribution chapter.

A script (future) would support top-level statements that execute in order, with the compiler wrapping them in a synthetic main().

The Three-Layer Model

Pluto programs are organized around three layers, each addressing a different concern:

Layer 1: Classes are the workhorses. They hold state, define behavior, declare dependencies, and enforce contracts. A class does not know how it is orchestrated – OrderProcessor works the same whether it is called from an HTTP handler, a queue consumer, or a test.

Layer 2: Stages define how a program runs. They wire together the classes that do the actual work. The critical constraint: stages have DI but no fields. They cannot hold state. All state lives in the injected classes. This prevents stages from becoming god objects.

Layer 3: System defines the topology of a distributed application – which members exist and how they relate. system declarations are implemented: the compiler checks members against each other and emits one binary per member (see the Distribution chapter). Where members physically deploy remains configuration, not code.

Stages: Programmable Entry Points

Status: Partially implemented. stage declarations work today: requires fn lifecycle templates, inheritance (stage Worker : Daemon), override, and DI bracket deps merged across levels. Still planned: App as a stdlib-defined stage template, and instantiating a stage by its lowercased name (http_server UserApi { ... }). Examples below that use lowercased instantiation show the planned direction.

The app you have seen so far is actually the simplest stage. In the planned design, App is defined in the standard library:

stage App {
    requires fn main(self)
}

When you write app MyService[db: Database] { fn main(self) { ... } }, you are using the App stage. The keyword app is not special syntax – it is the lowercased name of the App stage template.

Stages support inheritance, allowing library authors to define reusable lifecycle templates:

stage Daemon {
    requires fn run(self)
    requires fn shutdown(self)

    fn main(self) {
        signal.on_sigterm(() => self.shutdown())
        self.run()
    }
}

stage HttpServer : Daemon {
    requires fn routes(self) Router
    requires fn port(self) int

    override fn run(self) {
        http.serve(self.port(), self.routes())
    }
}

Daemon defines a lifecycle: set up signal handling, call run(), shut down gracefully on SIGTERM. HttpServer inherits that lifecycle and overrides run() to serve HTTP. Users instantiate a stage by using its name as a keyword:

http_server UserApi[db: Database] {
    fn routes(self) Router {
        Router.new()
            .get("/users", self.list)
            .post("/users", self.create)
    }

    fn port(self) int { return 8080 }
    fn shutdown(self) { self.db.close() }

    fn list(self, req: Request) Response { ... }
    fn create(self, req: Request) Response { ... }
}

The compiler validates that all requires methods are implemented, resolves the full lifecycle chain, merges DI bracket deps from all levels, and generates a synthetic main().

More Stage Examples

Scheduled job – runs once and exits. External scheduler handles timing:

stage ScheduledJob {
    requires fn execute(self)

    fn main(self) {
        self.execute()
    }
}

scheduled_job DailyReport[db: Database, email: EmailService] {
    fn execute(self) {
        let data = self.db.aggregate_daily()!
        self.email.send_report(data)!
    }
}

Serverless handler – the platform owns the event loop:

stage LambdaHandler {
    requires fn handle(self, event: LambdaEvent) LambdaResponse

    fn main(self) {
        lambda.serve((event: LambdaEvent) => self.handle(event))
    }
}

lambda_handler ImageResizer[storage: S3Storage] {
    fn handle(self, event: LambdaEvent) LambdaResponse {
        let image = self.storage.get(event.key)!
        let resized = resize(image, 800, 600)
        self.storage.put(event.key + "_thumb", resized)!
        return LambdaResponse { status: 200 }
    }
}

Stages can be defined in the standard library, in third-party packages, or in your own codebase. An organization can define a CompanyApi stage that bakes in auth middleware, observability, and internal routing conventions – every new service inherits the pattern without reimplementing it.

Why Inheritance Works Here

Pluto classes do not support inheritance. Stages do. This is not a contradiction. Inheritance works well for stages because the hierarchy is naturally shallow (2-4 levels), each level refines a linear lifecycle (no diamond problem), and the base is a skeleton algorithm – the Template Method pattern – not a data container. Stages cannot hold fields, so the failure modes of classical inheritance (fragile base class, unclear ownership of mutable state) do not apply.

What the Compiler Does for You

To appreciate what the app model provides, consider what you do not write:

The app declaration is not just an entry point. It is a contract between the programmer and the compiler: “Here is what my program needs. Build it for me, and prove it is correct.”

Concurrency

Go popularized the idea that concurrency should be cheap and communication should use channels. Rust proved that compile-time analysis can eliminate data races. Java continues to evolve threading models with virtual threads and structured concurrency APIs. Each made a different tradeoff between safety, ergonomics, and performance.

Pluto takes a different position: you write normal classes, and the compiler figures out what needs synchronization. Tasks give you lightweight concurrency. Channels give you communication. Spawn arguments are deep-copied, so tasks cannot race on values. For shared state there are two mechanisms: DI singletons get compiler-inferred reader/writer locks from self vs mut self method signatures, and objects — entities — are shared by construct with serialized methods. No sync.Mutex, no Arc<RwLock<T>>, no synchronized blocks.

Tasks

Spawning and Joining

spawn takes a function call and runs it concurrently, returning a Task<T> handle:

fn double(x: int) int {
    return x * 2
}

fn main() {
    let t1 = spawn double(5)
    let t2 = spawn double(10)
    let t3 = spawn double(15)
    print(t1.get())
    print(t2.get())
    print(t3.get())
}

spawn returns immediately. The function executes on a separate thread. .get() blocks until the result is available. Void functions produce a Task<void> – call .get() to wait for completion even when there is no return value.

Error Handling

Errors flow through tasks transparently. If the spawned function can raise errors, .get() propagates them:

error NetworkError {
    message: string
}

fn fetch(url: string) string {
    if url == "" {
        raise NetworkError { message: "empty url" }
    }
    return f"response from {url}"
}

fn main() {
    let t = spawn fetch("https://example.com")
    let result = t.get()!
    print(result)
}

The compiler infers that fetch is fallible and therefore t.get() is fallible. You handle it with ! (propagate) or catch (handle locally), exactly like any other fallible call. No special error handling model for concurrent code.

Waiting

.get() blocks until the spawned function completes. There is no timeout variant – if you need bounded waiting, use channels with recv_timeout instead.

Channels

Channels are typed conduits for sending values between concurrent tasks. One end sends, the other receives.

Creating Channels

let (tx, rx) = chan<int>(10)

chan<T>(capacity) returns a (Sender<T>, Receiver<T>) pair. The capacity sets the buffer size – send blocks only when the buffer is full. chan<T>() with no argument defaults to capacity 1. This is the only destructuring form in Pluto – it is specific to chan, not a general tuple system.

Sending and Receiving

fn produce(tx: Sender<string>) {
    tx.send("hello")!
    tx.send("world")!
    tx.close()
}

fn consume(rx: Receiver<string>) {
    for msg in rx {
        print(msg)
    }
}

fn main() {
    let (tx, rx) = chan<string>(5)
    let p = spawn produce(tx)
    let c = spawn consume(rx)
    p.get()!
    c.get()
}

.send() blocks until there is space. .recv() blocks until a value arrives. Both raise ChannelClosed when the channel is closed. for-in over a receiver drains it until closed – this is the idiomatic consumption pattern.

For non-blocking operations, use try_send and try_recv:

tx.try_send(value)!      // raises ChannelFull if buffer is at capacity
let val = rx.try_recv()!  // raises ChannelEmpty if nothing available

Closing and Errors

tx.close() signals that no more values will be sent. Further sends raise ChannelClosed. Receivers drain buffered values first, then receive ChannelClosed. Three built-in error types cover all failure modes:

• ChannelClosed – channel was closed
• ChannelFull – non-blocking send on a full buffer
• ChannelEmpty – non-blocking recv on an empty buffer

These integrate with Pluto’s error system. The compiler infers them automatically – if your function calls tx.send(v)!, the compiler knows it can raise ChannelClosed.

Fan-In and Timeouts

Multiple senders can write to the same channel (fan-in). Timed operations bound how long a send or recv blocks:

tx.send_timeout(value, 1000)!   // block up to 1 second
let val = rx.recv_timeout(500)!  // block up to 500ms

Select

When you need to wait on multiple channels simultaneously, select provides multiplexing:

select {
    val = rx1.recv() {
        print(f"got int: {val}")
    }
    msg = rx2.recv() {
        print(f"got string: {msg}")
    }
    default {
        print("nothing ready")
    }
}

select evaluates whichever arm becomes ready first. The default arm executes if no channel is immediately ready. Without default, select blocks until at least one arm can proceed. If all channels are closed and no default is present, select raises ChannelClosed.

Inferred Synchronization

Tasks and channels handle most concurrency needs. But real backend systems also need shared state: a session cache, a rate limiter, configuration that updates at runtime.

Go solves this with sync.Mutex and discipline. Rust solves it with Arc<RwLock<T>>. Java solves it with synchronized. Pluto’s approach: the compiler already knows everything it needs to solve this automatically.

The Motivating Example

A service registry that syncs with discovery and serves lookups to concurrent handlers (a sketch — DiscoveryClient and RequestHandler left to the imagination):

class ServiceRegistry[discovery: DiscoveryClient] {
    services: Map<string, ServiceEndpoint>

    fn lookup(self, name: string) ServiceEndpoint? {
        return self.services[name]
    }

    fn refresh(mut self) {
        let latest = self.discovery.fetch_all()!
        self.services = latest
    }

    fn start_sync(mut self) {
        while true {
            self.refresh() catch err {
                print("sync failed")
            }
            sleep(30000)
        }
    }
}

app MyApp[registry: ServiceRegistry, handler: RequestHandler] {
    fn main(self) {
        let sync = spawn self.registry.start_sync()
        sync.detach()

        for conn in listen(8080) {
            spawn self.handler.handle(conn)
        }
    }
}

No shared keyword, no lock annotations. The compiler sees that ServiceRegistry is a DI singleton, lookup() is a self method called from request handler tasks, and start_sync() is a mut self method in a background task. It auto-wraps self methods with reader locks and mut self methods with writer locks. Hundreds of concurrent lookups proceed unblocked. The 30-second refresh briefly takes exclusive access.

How It Works

mut self is the universal lever. self methods are read-only – safe to call concurrently. mut self methods modify state – they require exclusive access. The compiler performs whole-program analysis:

1. Walk the DI graph and spawn sites.
2. Identify which singletons are reachable from concurrent contexts.
3. For each concurrently-accessed singleton, inject synchronization: reader locks on self methods, writer locks on mut self methods.

If a singleton is only accessed from one thread, no locks are generated. Zero overhead when concurrency is absent.

Compare what you write in Go – sync.RWMutex field, RLock()/RUnlock() in every reader, Lock()/Unlock() in every writer – or Java – ReentrantReadWriteLock, try/finally blocks wrapping every access. In Pluto, you write fn lookup(self) and fn refresh(mut self). The compiler handles the rest.

Channels vs Shared State

Use channels when data flows in one direction. Use DI singletons when wiring provides the shared state. Use an object when the sharing is the point — the entity is one thing, every task talks to the same one, and serialization is guaranteed by the construct rather than inferred from usage.

Copy on Spawn

When you spawn func(args), every argument is deep-copied into the spawned task. The task gets its own independent world:

let mut data = [1, 2, 3]
let task = spawn process(data)   // data is deep-copied
data.push(4)                     // caller's copy, unaffected
let result = task.get()          // task worked on its own copy

This eliminates data races on values by construction. The exceptions are the things that mean sharing:

• Objects are shared, never copied. An object is an entity — copying it would mint a second identity. Spawn hands the task the same entity, and sharing is safe because an entity’s methods are serialized per instance. This applies recursively: deep-copying a class value shares any entity nested inside it.
• Channels are shared by reference — that is the point of a channel.
• DI singletons are shared and auto-synchronized (above).
• Strings are pointer-copied because they are immutable.

Structured Concurrency

Task<T> is must-use. A task handle must be consumed via .get(), .detach(), or assignment. Dropping a handle is a compile error:

spawn work()                     // COMPILE ERROR: Task handle must be used

let task = spawn fire_and_forget()
task.detach()                    // OK: explicitly detached

Cancellation is cooperative. .cancel() sets a flag; a task that is cancelled before producing a result raises the built-in TaskCancelled error from .get():

let task = spawn long_work()
task.cancel()
let result = task.get() catch -1    // TaskCancelled surfaces here if it won the race

Cancellation races with completion — if the task finished first, .get() returns its result normally.

The pattern in the wild. Electronic trading runs this entire chapter by hand, at nanosecond stakes. Client order IDs are idempotency keys verbatim — the exchange dedups on them so a retried submit cannot double-fill. The cancel/fill race is the definite/ambiguous split every trader knows: “did my cancel win?” has three answers — cancelled, filled, unknown yet — and rounding the third to either of the others loses real money. Market data arrives sequence-numbered with gap-recovery protocols: monotone facts, safe to cache and share precisely because sequence numbers only grow. And every participant knows their market view is stale testimony by the time they act on it — the book moved while the packet flew. The constructs these desks enforce by convention are the subject of Verified Distribution.

The Full Picture

Pluto’s concurrency model is layered:

1. spawn + Task<T> – lightweight concurrency with error propagation, must-use handles, detach, and cooperative cancel.
2. Channels – typed, directional communication between tasks.
3. Copy-on-spawn – arguments deep-copied; data races on values are impossible by construction.
4. Inferred synchronization – the compiler auto-wraps concurrently-reachable DI singletons: reader locks on self methods, writer locks on mut self.
5. Objects – entities shared across tasks with per-instance serialized methods, by construct. See Objects and Entities.
6. Distributed replication (future) – the same mut self distinction extends to cross-pod state.

The goal is that adding concurrency to a Pluto program never requires restructuring your code. You do not wrap types in Arc<Mutex<T>>, you do not add synchronized blocks, you do not sprinkle sync.RWMutex fields into structs. You mark which methods mutate with mut self, and the compiler handles the rest.

Objects and Entities

Every backend program contains two kinds of things, and most languages refuse to distinguish them.

A Point { x: 1, y: 2 } is data. It is its bytes. Copy it and nothing is lost; compare it field-by-field and you have compared everything there is. If reading a field hit the network, you would be shocked.

A payment service, a live TCP connection, a counter shared between threads — these are not data. Each one is an entity: it represents the actual thing, not a snapshot of it. Calling a method is a message to the thing; its state may change between calls; copying it would be semantically wrong (two payment services? two owners of one socket?). Identity is the point.

Mainstream languages give you one construct for both and leave the distinction in your head. Java makes everything an identity-bearing object and then bolts on equals(), records, and value-type proposals to claw data semantics back. Go and Rust give you structs and leave “is this a value or a service?” as a convention. Pluto makes the distinction a declaration:

• class declares a value — structural equality, deep-copied across concurrency boundaries.
• object declares an entity — reference identity, shared across concurrency boundaries, methods serialized.

Declaring an object

An object body is syntactically a class body: fields, methods, bracket deps, invariants. The difference is entirely in the semantics the compiler attaches to instances.

object Counter {
    value: int

    fn increment(mut self) {
        self.value = self.value + 1
    }

    fn get(self) int {
        return self.value
    }
}

Equality says what you mean

Value equality is structural. Two points with the same coordinates are the same point — there is nothing else to a value than its content. This works recursively through classes, enums, arrays, maps, sets, and nullables.

Entity equality is identity. Two counters that both read zero are still two different counters:

class Point {
    x: int
    y: int
}

object Counter {
    value: int

    fn get(self) int {
        return self.value
    }
}

fn main() {
    let a = Point { x: 1, y: 2 }
    let b = Point { x: 1, y: 2 }
    print(a == b)        // true — same content, same value

    let c = Counter { value: 0 }
    let d = Counter { value: 0 }
    let alias = c
    print(c == d)        // false — same fields, different entities
    print(c == alias)    // true — one entity, two names
}

This composes: a structural comparison of two class values that each hold a Counter field compares those fields by identity. Equal state in a different entity is not the same entity.

The pattern in the wild. Transfusion medicine enforces entity-not-description with a wristband: blood is crossmatched for the patient wearing the band, not for anyone matching the chart’s description — identity, never field equality. The type-and-crossmatch result expires after 72 hours (evidence with a validity window, not a permanent fact about the patient), and the two-person bedside check is validation at the point of effect — the moment the blood hangs, not the moment it was ordered. Every piece of that protocol is a construct in this book; Verified Distribution makes the case that this is no coincidence.

Spawn: values copy, entities share

Pluto’s baseline concurrency rule is that spawn deep-copies its arguments. Each task gets its own world; data races on values are impossible by construction:

class Data {
    value: int

    fn bump(mut self) {
        self.value = self.value + 1
    }
}

fn work(mut d: Data) {
    d.bump()
}

fn main() {
    let mut d = Data { value: 0 }
    let t = spawn work(d)
    t.get()
    print(d.value)    // 0 — the task mutated its own deep copy
}

Objects invert the rule. The entity is one thing; a copy would mint a second identity, which is exactly wrong. So spawn shares entities — and sharing is safe because objects carry a stronger concurrency contract: an object’s methods are serialized. Each instance processes one message at a time (a per-instance lock; distinct instances of the same type run concurrently). You get shared state without a heuristic “did both threads touch it?” analysis — the guarantee is attached to the construct that means shared identity.

Serialized means one message at a time, not one stack frame. An entity method that calls another method on the same instance — directly, through an alias, through mutual recursion, even via at placement on itself — is still processing the same message, and the call proceeds. Reentrancy within a message is not a deadlock and not a second message; the serialization boundary sits between messages from outside the activation.

object Counter {
    value: int

    fn increment(mut self) {
        self.value = self.value + 1
    }

    fn work(mut self) {
        let mut i = 0
        while i < 1000 {
            self.increment()
            i = i + 1
        }
    }

    fn get(self) int {
        return self.value
    }
}

fn main() {
    let mut c = Counter { value: 0 }
    let t = spawn c.work()
    let mut i = 0
    while i < 1000 {
        c.increment()
        i = i + 1
    }
    t.get()
    print(c.get())    // 2000 — both sides hit the same entity, no lost updates
}

Write this with a class and the spawned task increments a private copy: you get 1000 and 1000, isolated. Write it with an object and you get one entity, 2000, and no data race — serialization is the construct’s guarantee, not your discipline.

The sharing rule follows the entity wherever it is nested: deep-copying a class value into a task shares any entity stored inside it. Values copy; entities ride along by reference.

The pattern in the wild. The famous LMAX architecture — an entire financial exchange matched on a single thread — is entity method serialization deployed at world scale. The matching engine is one entity: every order, every cancel, from every trader on earth, is a message to the same referent, processed one at a time. That is exactly why it needs no locks and loses no updates — the industry arrived at “serialize the authority, don’t lock the data” through measurement and production pain, and here it is the semantics of the object keyword. Verified Distribution collects this pattern library across industries.

Generic objects

Objects can take type parameters. Each monomorphized instantiation is a distinct entity type with its own identity space and its own per-instance serialization:

object Topic<T> {
    name: string
    latest: T?
    published: int

    fn publish(mut self, msg: T) {
        self.latest = msg
        self.published = self.published + 1
    }

    fn count(self) int {
        return self.published
    }
}

fn main() {
    let mut news = Topic<string> { name: "news", latest: none, published: 0 }
    let mut metrics = Topic<int> { name: "metrics", latest: none, published: 0 }
    news.publish("breaking")
    metrics.publish(42)
    print(news.count())      // 1
    print(metrics.count())   // 1
}

Topic<int> and Topic<string> are different entity types entirely — their values cannot even be compared.

Entities cross boundaries as handles

A class value crossing a placement boundary is copied — it is wire-shaped data. An entity cannot be copied without destroying what it means, so an entity crosses by reference: what serializes is an identity handle — the entity’s home process, its type, and a per-home id. The wire stays a closed, compiler-derived surface; a handle is just schema-level data.

Identity survives the round trip. Send an entity to a server that stores it and hands it back, and the caller gets the same entity — sent == returned is true.

Calling through an entity is a placement expression — at runs the call where the entity lives:

object Counter {
    value: int

    fn increment(mut self) {
        self.value = self.value + 1
    }

    fn get(self) int {
        return self.value
    }
}

fn main() {
    let mut c = Counter { value: 0 }
    at c { increment() } catch err {
        print("boundary failure")
        return
    }
    let n = at c { get() } catch -1
    print(n)    // 1
}

If the entity is local, at is a direct call. If it is a handle to an entity in another process, the same expression dials the entity’s home, and the entity’s own interface hash rejects version skew. Either way the boundary contract is identical — which is why every at must be handled with ! or catch: a domain boundary can fail in some deployment plan, even one that happens to be colocated today.

Distribution stays explicit. A plain method call on a foreign handle outside at is a runtime error — the visible at boundary is the point. The Distribution chapter covers placement, domains, and serving in full.

Which one do you want?

The standard library answers this consistently and it is a good guide:

• Shared resources are objects. net.TcpListener, net.TcpConnection, http.HttpServer, http.HttpConnection — each owns an OS resource with identity (a bound port, a live socket) that is genuinely shared: handed to spawned tasks, held across calls. Copying one would mean two owners of one descriptor; as entities they are spawn-shared and their methods serialize.
• Resource obligations are typestated values, not objects. fs.File<M, S> draws the line from the other side: an open file handle is not a thing to share but evidence you hold. The OS is the authority over the real file state; fs.open_read mints a linear, must-release capability (“I opened this and have not yet closed it”) that the compiler forces you to discharge — close(), or discard() after a failure poisons it. Sharing, the one thing entity semantics buy, is exactly what a file handle must not have; what it needs is a checked protocol, which is what a typestate is. The general factoring: entities are authorities — shared, identity-bearing, always answering with their current state — and typestated values are the evidence authorities issue: grants, leases, handles — linear, unsharable, honest about their staleness. See std.fs for the worked example.
• Service singletons are objects. A PaymentService, a served BillingService — one pool of funds with identity, mutations that must stick.
• Wire-shaped data stays classes. Request, Response, JSON values — snapshots, copied freely, compared structurally.
• Transient local cursors stay classes. Parsers and encoders in hot loops, where per-instance method serialization would cost and identity adds nothing.

A useful test from the DI system: anything that needs observable per-injection identity is, by definition, an entity. Values have no identity to observe.

No inheritance, still

Objects do not add inheritance. Entity semantics are about identity, sharing, and messaging — not a second polymorphism mechanism. Traits (including default methods) cover behavior specialization and subtype polymorphism for objects exactly as they do for classes.

Typestates

Every API has a protocol. A partition must be acquired before it is consumed. A lease must be released. A connection must be opened before it is read. Most languages document the protocol in prose, check it at runtime if you are lucky, and let you find out in production if you are not.

Pluto makes protocol violations inexpressible. A state is a type parameter; a method that is only legal in some state only exists in that state; a transition consumes the old binding so stale references cannot be reused. Calling out of order is not a runtime error — it is a method that does not exist, or a binding that is no longer there.

State-gated methods

A typestate is an ordinary generic class whose type parameter encodes the state. States are plain marker classes. A where S == State clause after a method’s return type restricts the method to one state:

class Unowned { tag: int }
class Owned { tag: int }

class Partition<S> {
    id: int

    fn acquire(self) Partition<Owned> where S == Unowned {
        return Partition<Owned> { id: self.id }
    }

    fn consume(self) int where S == Owned {
        return self.id
    }

    fn release(self) Partition<Unowned> where S == Owned {
        return Partition<Unowned> { id: self.id }
    }

    fn describe(self) string {       // no clause: exists in every state
        return f"partition {self.id}"
    }
}

fn main() {
    let u = Partition<Unowned> { id: 7 }
    let o = u.acquire()
    print(o.consume())    // 7
}

Method existence is per-instantiation. When Partition<Owned> is instantiated, only methods whose constraints are satisfied get registered; monomorphization never even generates the excluded ones. Calling consume() on a Partition<Unowned> is not a “constraint violation” — the method is simply not there, and the diagnostic says why:

error: method 'consume' does not exist on 'Partition<Unowned>':
on 'Partition' it exists only where S == Owned

Functions express state requirements with ordinary parameter types — fn process(p: Partition<Owned>) needs no special syntax. Passing a Partition<Unowned> is a plain type mismatch.

Transitions consume their receiver

Gating methods by state is only half the guarantee. After let o = u.acquire(), what stops you from calling u.acquire() again — a stale alias in the pre-transition state?

Linearity does. A transition method is one whose return type is the same class with a state parameter changed (Partition<Unowned> → Partition<Owned>). Calling a transition through a local binding consumes that binding; later uses are compile errors:

let u = Partition<Unowned> { id: 7 }
let o = u.acquire()
let o2 = u.acquire()    // COMPILE ERROR

error: 'u' was consumed by the transition '.acquire()' (it is now
Partition<Owned>); use the transition's result, or rebind 'u'

The discrimination is automatic and surgical: only type parameters that appear in a where clause count as state parameters, so data generics never participate — Box<T>.map() returning Box<U> consumes nothing, and a class with no where clauses is untouched by the analysis. Reassignment or a fresh let revives a consumed binding. Branch joins are conservative (consumed on any path means consumed after the join), loops are analyzed to a fixpoint (a transition in iteration one is caught as a use in iteration two), and capturing a consumed value in a closure or spawn is a use.

Must-release states

Some states are not just restrictive — they are obligations. Holding a lease means you owe a release. Pluto lets the class say so:

class Idle { tag: int }
class Held { tag: int }

class Lease<S> {
    id: int

    must_release Held

    fn acquire(self) Lease<Held> where S == Idle {
        return Lease<Held> { id: self.id }
    }

    fn release(self) Lease<Idle> where S == Held {
        return Lease<Idle> { id: self.id }
    }
}

A binding in a must_release state is fully linear. Dropping it — by fall-through, return, break, rebinding, or just never touching it again — is a compile error:

fn main() {
    let l = Lease<Idle> { id: 7 }
    let h = l.acquire()
    print("done")        // COMPILE ERROR: h was never discharged
}

error: 'h' still holds Lease<Held>, a must_release state, when it goes
out of scope; transition it out of 'Held' (e.g. .release()), move it
onward, or return it

The diagnostic computes the suggested exits from the class’s own transitions. The rules:

• Moves travel the obligation. let b = a, passing as an argument, returning, and raising inside an error payload each move the value — the caller is clean, and the receiver now owes the discharge. One obligation, one owner, always.
• Capture is rejected. A closure or spawn capturing a live must-release binding would duplicate the evidence.
• Field and container stores are rejected. The obligation would escape the analysis.
• Discharge is a consuming transition out of the state, moving the value onward, or returning it.

The pattern in the wild. Electrical lockout-tagout is must-release linearity made of steel. Before working on a circuit, a worker hangs a personal padlock and tag on the breaker: a token you hold in your hand, and re-energization is impossible until you remove it — nobody else’s key fits. The multi-padlock hasp goes further: every worker on the job locks the same hasp, and the breaker cannot close until all locks come off. That shape — conjunctive linear obligations, N holders, all must release — is one Pluto does not have yet; must_release tracks a single owner. Breaker interlocks (“cannot close unless proven de-energized”) are the other half of the pattern: the effect site dominated by a validity check. Verified Distribution traces both shapes across the industries that invented them.

Degradation: when the world moves you out of a state

Transitions so far are things you do. Distribution adds transitions the world does: the coordinator revokes your lease between two instructions, and no local type can prevent it. Pluto’s answer is state-carrying errors — a fallible transition whose error carries the value in its post-failure state:

class Idle { tag: int }
class Held { tag: int }
class Revoked { tag: int }

error Degraded { lease: Lease<Revoked> }

class Lease<S> {
    id: int
    epoch: int

    must_release Held

    fn acquire(self) Lease<Held> where S == Idle {
        return Lease<Held> { id: self.id, epoch: self.epoch + 1 }
    }

    fn renew(self) Lease<Held> where S == Held {
        if self.epoch > 2 {
            raise Degraded { lease: Lease<Revoked> { id: self.id, epoch: self.epoch } }
        }
        return Lease<Held> { id: self.id, epoch: self.epoch + 1 }
    }

    fn release(self) Lease<Idle> where S == Held {
        return Lease<Idle> { id: self.id, epoch: self.epoch }
    }

    fn describe(self) string {
        return f"lease {self.id} (epoch {self.epoch})"
    }
}

Because Degraded’s payload is the receiver’s class at a changed state (Lease<Revoked> vs the receiver’s Held), the compiler discriminates it as a degradation error — the exact mirror of the transition rule. That drives the error-path bookkeeping:

fn main() {
    let l = Lease<Idle> { id: 7, epoch: 0 }
    let h = l.acquire()

    let h2 = h.renew() catch e: Degraded {
        print(f"degraded: {e.lease.describe()}")
        return
    }

    let done = h2.release()
    print(f"released: {done.describe()}")
}

Raising a degradation error moves the receiver into the payload. Catching one therefore consumes the receiver on the error path only: inside the handler the old binding is gone and the degraded value lives in e.lease; a handler that terminates (return, raise, break) leaves the success path’s binding valid with no ceremony. Recovery is just reading the payload out — let stale = e.lease.

The obligation survives the failure. If the payload’s state is itself must-release, wildcard and shorthand catches are rejected (they would strand the payload); a typed handler takes the obligation on as e.field. In practice degraded states like Revoked are droppable — “the world took it from you” should not pile ceremony on the recovery path — while only Held-like states carry obligations. Note the design cut: release() transitions out of Held and the degraded value needs no release, because “clean up your local belief” is the one duty the world cannot revoke.

What a typestate honestly claims

Lease<Held> does not mean “the coordinator still considers me the holder.” It means “I acquired and have not released” — a record of your own actions, which nothing outside the process can falsify. That is the only kind of fact a static type can honestly carry in a distributed system; remote agreement can be revoked between any two instructions, which is exactly why revocation surfaces as a typed, catchable Degraded error rather than being promised away by the type.

The same reasoning explains a rule you will notice: typestate never lives on an object. Entities are the sharing construct — if another task transitions a shared entity, your binding’s static state would be a lie. The factoring that works: the entity is the authority (shared, always answering with its current opinion), and typestated values are evidence it issues — grants, leases, tokens — linear, possibly must-release, honest about their staleness, validated by the authority at the point of effect. The Verified Distribution chapter develops this into Pluto’s larger direction.

Contracts

Most languages punt on correctness. You write code, you write tests, and you hope the gap between what you intended and what you shipped is small. The available tools are underwhelming: assertions are ad hoc and stripped in release builds, property-based testing runs outside the program, and Eiffel-style contracts — where they exist at all — are runtime checks that crash after the bug has happened.

Pluto’s contract system takes the opposite position: contracts are specifications the compiler proves, not guards that crash. A class invariant is not checked at runtime — it is discharged at compile time, at every site that could break it, or the program does not compile.

Four primitives:

Plus assert, the explicit runtime check — which also establishes its condition as a fact for the prover afterward.

There is no runtime ensures. Postconditions exist only in proof form (more below).

Invariants are compile-time proofs

Declare an invariant inside a class body:

class Account {
    balance: int

    invariant self.balance >= 0

    fn deposit(mut self, amount: int)
        requires amount > 0
    {
        self.balance = self.balance + amount
    }

    fn withdraw(mut self, amount: int)
        requires amount > 0
        requires self.balance >= amount
    {
        self.balance = self.balance - amount
    }
}

fn main() {
    let mut account = Account { balance: 100 }
    account.deposit(50)
    account.withdraw(30)
    print(account.balance)    // 120
}

This compiles — and that is the whole story at runtime. There is no invariant check in the generated code, anywhere. The compiler proved, at compile time, that no execution of this program can make balance negative:

• The construction Account { balance: 100 } substitutes the initializer into the invariant: 100 >= 0. Proven.
• Inside deposit, the write is tracked symbolically: balance = old(balance) + amount. The entry facts are the invariant on self (old(balance) >= 0) and the requires (amount > 0). The sum is nonnegative. Proven.
• Inside withdraw, balance = old(balance) - amount with entry fact old(balance) >= amount. Proven.

The invariant may be broken temporarily between writes inside a mut self method; the proof obligations sit at the boundaries — method exits, raises, any statement containing a call (something might observe the object), loop entry and body end, branch joins. Foreign writes (obj.field = v from outside the class’s own methods) are proven immediately; external code gets no temporary-violation window.

A rejected write site

Delete the guard and the compiler rejects the program at the write site, not at 3 a.m. in production:

class Account {
    balance: int

    invariant self.balance >= 0

    fn drain(mut self, amt: int) {
        self.balance = self.balance - amt    // COMPILE ERROR
    }
}

error: cannot prove invariant 'self.balance >= 0' of class 'Account' holds
at the end of this method in method 'drain': at this point self.balance =
-amt + old(self.balance). The invariant may be broken temporarily between
writes, but must be re-established at every boundary (method exits, raises,
calls, loops, branch joins). Establish the missing bound before this point
with a guard, a 'requires' clause, or an 'assert'
(e.g. 'if amt <= self.balance { ... }')

The diagnostic names the invariant, the site, the symbolic state the prover reached, and the three ways to fix it. Any of them works:

fn drain(mut self, amt: int) {
    if amt >= 0 && amt <= self.balance {
        self.balance = self.balance - amt    // proven from the guard
    }
}

Construction sites carry the same obligation. An initializer the prover cannot bound is rejected:

class Account {
    balance: int

    invariant self.balance >= 0
}

fn make(b: int) Account {
    return Account { balance: b }    // COMPILE ERROR: b is unbounded
}

error: cannot prove invariant 'self.balance >= 0' of class 'Account' for
this construction: the field initializers are not statically known to
satisfy it. Establish the needed facts before constructing — a guard
('if x >= 0 { ... }'), an 'assert', or a 'requires' clause on the
enclosing function — or simplify the initializers to expressions the
prover can bound

fn make(b: int) Account {
    assert b >= 0                    // runtime check; prover fact afterward
    return Account { balance: b }    // proven
}

There is no fallback mode. An invariant the compiler cannot discharge is a compile error — never a runtime residual, never undefined behavior. Unprovability costs you a guard or a requires clause, not a crash path.

ensures and old(): two-state proofs

An invariant says what is always true. An ensures clause says what a method did: it relates the receiver’s exit state to its entry state, with old(expr) naming the value expr had when the method was entered.

class Account {
    balance: int

    invariant self.balance >= 0

    fn deposit(mut self, amount: int)
        requires amount > 0
        ensures self.balance == old(self.balance) + amount
    {
        self.balance = self.balance + amount
    }
}

fn main() {
    let mut account = Account { balance: 100 }
    account.deposit(50)
    print(account.balance)    // 150
}

Like invariants, this is a compile-time obligation, discharged by the same symbolic machinery — the one that was already tracking balance = old(balance) + amount through the body. The clause must be proven at every normal exit of the method; a body that does not establish the declared relation is rejected with the symbolic state the prover reached:

class Counter {
    n: int

    fn bump(mut self) ensures self.n == old(self.n) + 2 {
        self.n = self.n + 1    // COMPILE ERROR
    }
}

error: ensures clause 'self.n == old(self.n) + 2' of method 'bump' of class
'Counter' is violated at the end of this method: at this point
self.n = old(self.n) + 1

Raise paths are exempt — a method that raises did not do what it promised, and the error contract governs those edges instead.

Callers assume the relation. This is the half that pays rent. Without ensures, a method call is opaque to the prover — once it returns, all the caller knows about the receiver is its invariant. With a declared ensures, the caller keeps the exact two-state relation across the call, and that fact feeds every downstream proof:

class Pos {
    v: int

    invariant self.v >= 1
}

class Counter {
    n: int

    invariant self.n >= 0

    fn bump(mut self) ensures self.n == old(self.n) + 1 {
        self.n = self.n + 1
    }
}

fn make(mut c: Counter) Pos {
    c.bump()
    return Pos { v: c.n }    // proven: n == old(n) + 1 and old(n) >= 0, so n >= 1
}

fn main() {
    let mut c = Counter { n: 5 }
    let p = make(c)
    print(p.v)    // 6
}

Delete the c.bump() call and the construction stops compiling — n >= 0 alone cannot prove v >= 1. The assumption really flows from the callee’s contract, not from wishful thinking. Sibling calls compose the same way: a double_bump that calls bump() twice proves ensures self.n == old(self.n) + 2 from the parts.

Two honest limits. ensures lives on class and object methods only — a free function has no receiver state to relate. And a call to anything other than a sibling method with its own declared ensures conservatively severs exact two-state knowledge mid-body (the callee might reach the receiver through an alias); the prover re-anchors to invariant-level facts after it.

Two-state invariants: monotonicity without a keyword

old() is also legal in an invariant — turning it into a relation that every state change must respect:

object Epoch {
    e: int

    invariant self.e >= old(self.e)

    fn advance(mut self) {
        self.e = self.e + 1    // proven: e + 1 >= e
    }

    fn now(self) int {
        return self.e
    }
}

self.e >= old(self.e) is monotonicity — the epoch never decreases — stated with no new keyword. The obligation sites are the same ones single-state invariants already carry: every mut self method exit is checked against the method’s entry state, and every foreign write against the pre-write state. A method that could ever move the field backward is a compile error:

fn reset(mut self) {
    self.e = 0    // COMPILE ERROR
}

error: cannot prove invariant 'self.e >= old(self.e)' of class 'Epoch' holds
at the end of this method in method 'reset': at this point self.e = 0. The
invariant may be broken temporarily between writes, but must be re-established
at every boundary (method exits, raises, calls, loops, branch joins).
Establish the missing bound before this point with a guard, a 'requires'
clause, or an 'assert' (e.g. 'if amt <= self.balance { ... }')

Construction has no pre-state, so two-state clauses impose nothing there — any initial value is legal; the relation binds every change after birth. This is the proof shape behind epochs, versions, sequence numbers, and high-water marks: a fencing design is only sound if a minted token can never become current again, and that sentence is now a clause the compiler checks rather than a comment reviewers hope stays true.

guarded_by: every write provably fenced

The third proof shape is about control flow rather than arithmetic. A field can declare that no write to it may ever escape a validity check:

error StaleGrant {
    token: int
    epoch: int
}

class WriteGrant {
    token: int
}

object Store {
    data: bytes guarded_by (g: WriteGrant) g.token == self.epoch
    epoch: int

    fn grant_write(mut self) WriteGrant {
        self.epoch = self.epoch + 1
        return WriteGrant { token: self.epoch }
    }

    fn apply(mut self, grant: WriteGrant, d: string) {
        if grant.token != self.epoch {
            raise StaleGrant { token: grant.token, epoch: self.epoch }
        }
        self.data = d.to_bytes()    // proven: dominated by the fence
    }

    fn read(self) string {
        return self.data.to_string()
    }
}

The clause reads: every write to self.data must be dominated by a conditional the prover can show implies g.token == self.epoch for some in-scope WriteGrant. In apply, the raise-guard is exactly that conditional — on the fall-through path, grant.token == self.epoch is a fact, and it survives to the write. This is the fencing pattern: grant_write advances the epoch, silently invalidating every older grant, and the fence rejects stale writers at the point of effect with a typed error.

Remove the fence — or move the write above it, or put a call between them that could disturb the compared fields — and the program stops compiling:

fn apply(mut self, grant: WriteGrant, d: string) {
    self.data = d.to_bytes()    // COMPILE ERROR: no fence dominates this write
}

error: cannot prove guard 'data' guarded_by (g: WriteGrant) g.token ==
self.epoch of class 'Store' at this write: no dominating check implies the
predicate for any in-scope 'WriteGrant' value (tried 'grant'). Every write to
a guarded field must be dominated by a conditional the prover can carry to
the write — e.g. a check of 'grant' whose failing path raises or returns,
placed before the write — and the facts it establishes must survive to the
write site (they are invalidated by calls that may run user code, loop
boundaries, and writes to the compared fields)

The details that make this sound: a guarded field may only be written through self, inside its class’s own methods — the write-set is closed, so the proof covers every write in the program. On an object, method serialization closes the check-then-act window (nothing interleaves between fence and write); on a value class the clause is sound because values do not share. And the binder must be a concrete value class — evidence you hold, not an entity whose fields can change under you.

Together, a two-state invariant and a guarded_by turn a fencing protocol’s safety theorem into compiled fact: the epoch only increases, and no write lands without a currently-valid grant. The repository’s examples/blob is the full protocol — a lockless single-writer blob store whose safety claim is no longer “by inspection” anywhere; see Verified Distribution for why that theorem is the load-bearing one.

The provable fragment

Because unprovable means rejected, every proof-form clause is restricted to what the flow-fact engine can decide — no SMT solver, no timeouts, no proofs that sometimes work:

Allowed in invariant: &&, ||, ! over integer comparisons (==, !=, <, >, <=, >=), where each side is linear arithmetic (+, -, * by a constant) over int literals and direct int fields of self — self.balance >= 0, self.lo <= self.hi, self.applied <= self.epoch — plus old(...) of those fields for two-state relations.

Allowed in ensures: the same shape, over the class’s own int fields, the method’s int parameters, and old(...) of those — self.balance == old(self.balance) - amt. (.len() terms are excluded from ensures for now: every collection mutation is an opaque call that severs the entry relation, so no len() postcondition could be proven today.)

Allowed in guarded_by: the same comparison shape, whose leaves are the class’s own int fields (self.epoch) and one-level int fields of the binder (g.token).

Rejected at declaration: float, string, or boolean properties; .len() and any method call; indexing; nested field access (self.child.value); non-linear arithmetic, division, modulo; any of these clauses on generic classes. ensures additionally rejects free functions — there is no receiver state to relate.

class User {
    name: string

    invariant self.name.len() > 0    // COMPILE ERROR
}

error: invariant 'self.name.len() > 0' is outside the provable fragment:
'.len()' — collection and method facts are not provable. Invariants are
compile-time proof obligations; they must be built from &&, ||, ! over
integer comparisons of linear arithmetic over the class's own int fields
(e.g. 'self.balance >= 0', 'self.lo <= self.hi'). Properties outside this
fragment cannot be statically discharged and are rejected

The fragment grows deliberately, one proof shape at a time. Predictability beats power: a prover that sometimes times out teaches people to distrust it.

What the prover knows

At any program point, the facts available for discharge are:

• requires clauses of the enclosing function — checked at runtime on entry, assumed by the prover inside the body.
• Invariants of class-typed parameters — any Account you receive already satisfies its invariant.
• if guards — flow facts, the same machinery that narrows nullables. Inside if amt <= self.balance { ... } the prover knows amt <= balance.
• assert statements — after an assert passes, the condition is a fact.
• ensures of called methods — after c.bump(), the declared two-state relation on c is a fact (see above).

The same flow-fact engine also flags conditions it can prove degenerate — warning: condition is always false on a branch that contradicts facts already established — so dead guards surface instead of silently papering over logic errors.

DI construction: the zero-state proof

Instances synthesized by dependency injection never pass through a struct literal — they are allocated zero-initialized and only their injected dep fields are wired. So a DI-constructed class may only carry invariants its zero state satisfies: invariant self.count >= 0 proves for a DI singleton; invariant self.count > 0 is a compile error. A class whose invariant needs nonzero initial state belongs outside startup wiring — give it a scoped lifecycle and seed it in a scope block, where the seed’s struct literal carries the ordinary construction proof.

requires: runtime at entry, fact inside

requires semantics are unchanged from the runtime-contracts era: clauses are evaluated at function entry, and a violation is a hard abort —

fn safe_divide(a: int, b: int) int
    requires b != 0
{
    return a / b
}

fn main() {
    print(safe_divide(10, 0))    // aborts
}

requires violation in safe_divide: b != 0

A violated precondition means the caller’s logic is wrong — not “the network is down,” which is what typed errors are for. Aborting beats continuing with corrupted assumptions, and contracts are never stripped from production builds.

Inside the body, requires clauses are entry facts for the prover — the withdraw example above is provable precisely because of its requires. Static discharge of requires at call sites (proving the caller meets them, eliminating the entry check) is planned; the proof engine it needs is the one already shipping for invariants.

Trait methods can carry requires, inherited and enforced for every implementation. Implementations cannot add their own — demanding more than the trait promised would break substitutability, and the compiler rejects it:

error: method 'process' on class 'MyProcessor' cannot add 'requires'
clauses: it implements trait 'Processor' and adding preconditions would
violate the Liskov Substitution Principle

assert: the escape hatch

assert is for facts the prover cannot establish — typically values from outside the program:

fn divide(a: int, b: int) int
    requires b != 0
{
    return a / b
}

fn main() {
    let input = 7            // imagine: read from stdin
    assert input != 0        // runtime check
    print(divide(10, input)) // prover accepts: the assert established it
}

It generates a runtime check, aborts on failure, and feeds the condition to the prover as a fact. Use it at trust boundaries; prefer guards and requires everywhere else.

Why no runtime ensures

ensures in Pluto is a proof, never a check. The runtime postcondition of Eiffel and D — evaluate the clause on exit, crash if false — remains rejected by design: it is exactly the crash-after-the-fact checking the proof system exists to eliminate. There is no mode in which an ensures compiles into generated code; an ensures the compiler cannot discharge is a compile error, same as an invariant.

The division of labor: what a method guarantees about how state changed is an ensures (proven at its exits, assumed by callers); what a function guarantees about its result is a return type — construct a PositiveBalance and its invariant is the postcondition, proven at the construction site.

The one runtime validation point: the wire

Inside a compiled program, invariants need no checks — every write path was proven. But data entering the program over a placement or serve boundary was not produced by your proven write paths. It is testimony, not proof.

So wire decode is the single place invariant validation runs at runtime: decoding a value of an invariant-carrying class re-checks the invariants and raises the standard wire error on violation — a typed error, mandatory to handle like any other boundary failure. A peer running skewed code, or a hand-crafted payload, cannot inject a balance: -5 into a program whose compiler proved balance >= 0 everywhere.

One trust boundary, one check, typed and catchable. Everywhere else: proofs.

The pattern in the wild. You already know this bug — the web ships it. A TLS certificate is a lease: evidence with a validity window. Web revocation is famously broken precisely because it is poll-based — browsers act on beliefs that outlive their warrants, and when the revocation check doesn’t answer, they soft-fail and trust the stale belief anyway. OCSP stapling is the fix with the right shape: carry fresh evidence with the effect instead of hoping a cached belief still holds. Certificate Transparency logs are monotone append-only facts — safe to cache and gossip because nothing is ever retracted. And the CA’s issuance validation is the authority’s fence: judged by the party that owns the namespace, at the point of effect. Pluto’s wire check above is the same move at program scale — testimony validated where it enters, proofs everywhere inside — and Verified Distribution is the chapter-length version of “here is that bug as a type error.”

Proofs have consequences

Facts do not just gate writes — they flow into error inference. A guard that makes a callee’s raise impossible removes the handling obligation at that call site entirely — and so does an ensures: after c.bump() with ensures self.n == old(self.n) + 1, a callee that raises only when n < 1 needs no handler. See error-set shrinking in the Error Handling chapter.

Comparison

Eiffel asked the right question in the 1980s and answered it with runtime checks. Pluto’s answer is proofs: the invariant you declare is the invariant the compiler discharges — and the diagnostic you get when it can’t is the specification of exactly what your code failed to establish.

Distribution: Placement, Domains, and Stages

Pluto is not an RPC language. It does not try to make network calls look local — that trick papers over exactly the things distributed programmers must design for: placement, data movement, partial failure, and the call that fails without telling you whether it executed.

Pluto is a distributed language. The central principle:

Logical distribution is part of the program. Physical deployment is not.

Most systems collapse three concerns: what computation happens, which domain owns it, and which process/pod/region runs it. Pluto puts the first two in the program and leaves the third to the deployment binding — the way a database separates the logical query from its physical execution plan. A program can be split apart or collapsed together without rewriting business logic, because the code never said “make an HTTP call”; it said where the computation belongs.

Placement: at

A placement expression evaluates its body in another logical execution domain:

import std.wire

error PaymentDeclined {
    code: int
}

// The payment service is an entity — THE payment domain's capability,
// not a copyable value — so it is an object (see Objects and Entities).
object PaymentService {
    fn charge(self, amount: int) int {
        if amount > 100 {
            raise PaymentDeclined { code: 402 }
        }
        return amount * 2
    }
}

app Shop[pay: domain PaymentService] {
    fn main(self) {
        let charged = at self.pay {
            charge(21)
        } catch err: PaymentDeclined {
            0 - err.code
        } catch err {
            -1
        }
        print(f"charged: {charged}")
    }
}

pay: domain PaymentService declares a dependency on the payment domain. at self.pay { charge(21) } means: evaluate this call in that domain. It does not mean “make an RPC call.”

How the boundary is physically crossed is the deployment binding’s decision, made at startup — not a code change:

# Plan A — colocated: the domain is wired in-process, at is a direct call
$ ./shop

# Plan B — distributed: the domain lives in another process
$ PLUTO_DOMAIN_PAYMENTSERVICE=127.0.0.1:9000 ./shop

Same binary. Same semantics. The compiler checks the boundary contract identically in both plans: values crossing must be wire-shaped, errors are typed and inferred across the boundary, and the at must be handled with ! or catch — because a domain boundary can fail in some deployment plan, even one that happens to be colocated today. Distribution is explicit — at is a visible, syntactic boundary — but transport is never the programming model.

Serving a domain

The other side of Plan B is a process that serves the domain’s entity:

import std.wire

error PaymentDeclined {
    code: int
}

object PaymentService {
    fn charge(self, amount: int) int {
        if amount > 100 {
            raise PaymentDeclined { code: 402 }
        }
        return amount * 2
    }
}

fn main() {
    let svc = PaymentService {}
    serve svc on 0    // port 0: OS-assigned, printed at startup
}

serve runs one thread per connection, so state mutated by a handler sticks — which is the point of calling an entity at home. The served object’s methods serialize per instance (they always do — it is an entity), so concurrent connections cannot interleave mid-method.

Typed errors cross the boundary: the client’s catch err: PaymentDeclined above works identically whether the decline came from an in-process call or over a socket. And every boundary is guarded by interface hashing — a caller and callee built from skewed versions of the interface are rejected at the boundary instead of silently mis-decoding each other’s data.

Entities cross as handles

Wire-shaped class values cross a boundary by copy. Entities cross by reference: what serializes is an identity handle (home process, type, id), and calling through a handle is placement — at entity { method() } runs the call where the entity lives. A server can accept an entity handle, store it, hand it back, and the caller gets the same entity — identity survives the round trip. Plain method calls on a foreign handle outside at are runtime errors: the boundary stays visible. See Objects and Entities.

Stages: lifecycle shells

A stage is a declaration for a deployable unit’s lifecycle: a shell with DI dependencies and a main, but no state of its own. Stages support requires fn members — lifecycle templates that concrete stages fill in:

class Config {
    fn db_url(self) string {
        return "postgres://localhost/mydb"
    }
}

class Database[config: Config] {
    fn query(self, sql: string) string {
        return f"result: {sql} (db={self.config.db_url()})"
    }
}

// Abstract base stage — defines the lifecycle template
stage Daemon {
    requires fn start(self)
    requires fn run(self)
    requires fn stop(self)

    fn main(self) {
        self.start()
        self.run()
        self.stop()
    }
}

// Concrete stage — inherits the lifecycle, adds DI
stage Worker : Daemon [db: Database] {
    override fn start(self) {
        print("Worker starting...")
    }

    override fn run(self) {
        print(self.db.query("SELECT * FROM jobs"))
    }

    override fn stop(self) {
        print("Worker stopped.")
    }
}

Each stage gets its own dependency graph, allocated when its process starts. Stages are one piece of the distribution story — the lifecycle/packaging piece — not the whole of it; the programming model for crossing boundaries is at over domains.

Systems: the whole program, checked

A system declaration names a set of modules that deploy together, and the compiler checks them against each other before any binary exists:

// main.pt
import billing
import orders

system Shop {
    billing: billing
    orders: orders
}

The orders module declares a remote dependency (app OrdersApp[billing: remote BillingService]) against a local interface mirror; the billing module serves the real BillingService. Compiling the system verifies that the dependency is actually served, that the interfaces match, and that the error contracts line up — then produces one binary per member:

$ pluto compile main.pt -o build --stdlib stdlib
  compiled billing → build/billing
  compiled orders → build/orders
system: 2 member(s) compiled

There is no gRPC schema to drift out of date, no Swagger spec to trust. The types match because one compiler checked both sides.

A note on remote: it is the first physical transport, shipped and working — but it couples the transport decision into the code, which is exactly what the placement model removes. at over logical domains is the target programming model; expect remote-style explicit wiring to be subsumed by it.

What at buys you that RPC frameworks don’t

Because the boundary is a language construct, the compiler checks what programmers otherwise track by convention:

• Value transfer — only wire-shaped data crosses by copy; entities cross as handles; anything else is rejected at compile time.
• Typed failure — the callee’s error set flows into the caller’s, plus the boundary’s own failure modes, and handling is mandatory. There is no “forgot to handle the network error.” And the boundary’s own failure is honest about what is known: every NetworkError carries a definite classification — the request provably never dispatched, or sent with no answer.
• Version skew — interface hashes are checked at the boundary, not discovered as corrupted decodes.
• Semantics under colocation — fusing two domains into one process is an optimization, and it is only legal if it preserves boundary semantics: no shared mutable references appear across a boundary that would have copied, and code written to survive an unreachable domain keeps that failure mode in its contract.

An at boundary can also fail ambiguously — the request left, no answer returned, and the effect may or may not have applied. No local check can resolve that; it is part of the boundary’s contract, and it is precisely what “RPC looks local” hides. Two pieces of making ambiguity first-class have shipped: the definite/ambiguous split itself, carried truthfully on every boundary failure as NetworkError.definite, and compiler-proven fencing via guarded_by — the examples/blob store’s single-writer safety theorem is now fully compiler-checked, not held by inspection. The remaining layer — idempotency and its kin as library-defined properties a retry combinator can demand — is the subject of Verified Distribution.

Where this is going

Shipped and tested today: whole-program compilation across service code, at placement over domain dependencies with deployment-plan binding, serve, typed errors across boundaries with definite/ambiguous failure classification, the schema-level wire format, interface hashing, entity handles, stages, and systems.

Deliberately open, and stated as such: what exactly declares a logical domain, the deployment-plan artifact that binds domains to physical placement, deadline and cancellation propagation, the precise legality rules for fusing domains, and structured distributed computation (parallel at, scatter/gather). The model these will land in — logical placement, physical execution — is settled; the pieces arrive incrementally, each checked by the same compiler that sees both sides of every boundary.

Syntax at a Glance

Compressed reference for variables, functions, operators, control flow, and builtins. No semicolons – Pluto uses newline-based statement termination. Comments with // only (no block comments).

Variables

let x = 42              // inferred as int
let x: int = 42         // explicit type annotation
let pi = 3.14           // float (f64)
let name = "alice"      // string
let flag = true         // bool
let b = (65).to_byte()  // byte (0-255, unsigned)

Variables are immutable by default – reassigning a plain let is a compile error. Declare with let mut to allow reassignment:

let mut x = 1
x = 2
x = x + 10

Primitive Types

Numeric literals support underscores: 1_000_000, 1_000.50. Hex literals: 0xFF, 0x0A.

Type Conversions

Explicit only, as named methods. No implicit coercion and no as cast. Widening conversions are total; a conversion that can lose information returns a nullable, which the compiler narrows to a plain value where it can prove the input is in range (a literal, a guard, a mask).

(42).to_float()          // int -> float
(3.14).to_int()          // float -> int?  (none for NaN/inf/out of range; truncates toward zero)
true.to_int()            // bool -> int (true = 1, false = 0)
n != 0                   // int -> bool is just a comparison
(255).to_byte()          // int -> byte?  (none outside 0..255; a literal narrows to byte)
(300).low_byte()         // int -> byte, keeping the low 8 bits by name
b.to_int()               // byte -> int (zero-extends)
"42".to_int()            // string -> int?  (none if it does not parse)

Operators

Arithmetic (int and float):

Increment/decrement (int only): x++, x--

Comparison (returns bool): ==, !=, <, >, <=, >=

Logical (bool only): &&, ||, !

Bitwise (int only): & (AND), | (OR), ^ (XOR), ~ (NOT), << (shl), >> (shr). Precedence: & > ^ > |.

Functions

fn add(a: int, b: int) int {
    return a + b
}

fn greet(name: string) {
    print(f"hello {name}")
}

Void functions omit the return type. All non-void paths require an explicit return – no implicit return of the last expression. Trailing commas allowed in argument lists.

String Interpolation

Arbitrary expressions inside {} within an f-prefixed string. A plain "..." string never interpolates – f"{x}" is the literal text {x}.

print(f"hello {name}")          // hello alice
print(f"{a} + {b} = {a + b}")   // 1 + 2 = 3
print(f"use {{braces}}")        // use {braces}  (escape with doubling)

Supports int, float, bool, string, byte. Class instances cannot be interpolated.

Escape sequences: \n, \r, \t, \\, \"

Control Flow

if / else if / else:

if x > 10 {
    print("big")
} else if x > 0 {
    print("small")
} else {
    print("non-positive")
}

while:

let i = 0
while i < 10 {
    print(i)
    i++
}

for-in – arrays, ranges, and strings:

for x in [1, 2, 3] {           // array iteration
    print(x)
}

for i in 0..10 {               // exclusive range: 0..9
    print(i)
}

for i in 0..=10 {              // inclusive range: 0..10
    print(i)
}

for c in "abc" {               // string: yields one-byte strings
    print(c)
}

Range endpoints can be expressions: for i in 0..(n * 2) { ... }

break / continue: work in both while and for. break exits the innermost loop. Cannot be used inside closures.

Generators

A function whose return type is stream T is a generator. Calling it creates the stream without running the body. Each turn of a for loop over the stream runs the body up to its next yield, which hands one value to the loop.

fn evens(limit: int) stream int {
    for i in 0..limit {
        if i % 2 == 0 {
            yield i
        }
    }
}

fn main() {
    for n in evens(10) {
        print(n)            // 0, 2, 4, 6, 8
    }
}

• The stream ends when the body finishes or runs a bare return. A generator needs no return.
• yield can appear inside if, while, for and match arms, at any depth. It cannot appear inside a closure.
• Generators are lazy, so an infinite one is fine. A break in the consuming loop simply stops asking for values.
• A stream is single-pass. Iterating it a second time yields nothing, so call the generator again for a fresh stream.
• Generators can be generic and can consume other streams:

fn take<T>(s: stream T, count: int) stream T {
    let mut i = 0
    for x in s {
        if i >= count {
            return
        }
        yield x
        i = i + 1
    }
}

Generators must be top-level functions. A method cannot be a generator.

Builtins

Builtin names are reserved – user functions cannot shadow them.

Quick Comparison

Strings and Collections

Pluto’s built-in collection types: strings, byte buffers, arrays, maps, and sets. Plus std.collections for functional operations on arrays.

Strings

String literals use double quotes. Concatenation with +. Interpolation with {} inside an f-prefixed string; a plain string never interpolates.

let s = "hello " + "world"
let name = "alice"
print(f"hello {name}")          // hello alice
print(f"{1 + 2}")               // 3
print(f"use {{braces}}")        // use {braces}  (escape with doubling)
print(f"hello {name}")           // hello {name}  (no f prefix: literal braces)

Escape sequences: \n, \r, \t, \\, \"

Indexing returns a one-byte string (read-only; s[0] = "x" is a compile error). Strings are UTF-8 and indexed by byte, so a non-ASCII character such as é spans several indices:

let s = "hello"
print(s[0])                     // h

Iteration yields one-byte strings, so it splits multi-byte (non-ASCII) characters:

for c in "abc" {
    print(c)                    // a, b, c
}

String Methods

to_int() and to_float() return nullable types. Use ? to propagate:

fn parse(s: string) int? {
    let v = s.to_int()?
    return v * 2
}

Method chaining works naturally: " Hello ".trim().to_lower().contains("hello") returns true.

Bytes

The byte type is an unsigned 8-bit integer (0-255). No byte literal – convert from int with .to_byte(). It returns byte? in general (none outside 0..255), but a literal or a value proven in range narrows to a plain byte; .low_byte() keeps the low 8 bits of any int by name.

let b: byte = (0xFF).to_byte()
print(b.to_int())               // 255
print((300).low_byte().to_int()) // 44

Byte ordering is unsigned: (0xFF).to_byte() > (0x7F).to_byte() is true.

Byte Buffers

Create with bytes_new(). Type is bytes. Supports .push(), .len(), indexing (read/write), and iteration.

let mut buf = bytes_new()
buf.push((72).to_byte())
buf.push((105).to_byte())
print(buf.len())                // 2
print(buf[0].to_int())          // 72
buf[0] = (90).to_byte()         // index write

for b in buf {                  // iteration yields byte values
    print(b.to_int())
}

String conversion – roundtrips cleanly:

let buf = "Hello".to_bytes()
let s = buf.to_string()         // "Hello"

Arrays

Literal syntax with type [T]. All elements must have the same type.

let nums = [1, 2, 3]           // [int]
let names = ["a", "b"]         // [string]

Indexing (read and write) and iteration:

let a = [10, 20, 30]
print(a[0])                     // 10
a[1] = 99                       // index write

for x in a {
    print(x)
}

Array Methods

Arrays work as function parameters (fn f(a: [int])) and return values (fn f() [int]).

Maps

Hash maps with typed keys and values. Keys must be hashable: int, float, bool, string, byte, or enum.

let m = Map<string, int> { "a": 1, "b": 2 }
let empty = Map<string, int> {}

print(m["a"])                   // 1
m["c"] = 3                      // insert via index
m["a"] = 99                     // overwrite

Map Methods

Iteration via .keys() or .values():

for k in m.keys() {
    print(f"{k}: {m[k]}")
}

Sets

Unordered collections with unique elements. Same hashable constraint as map keys.

let s = Set<int> { 1, 2, 3 }
let empty = Set<string> {}

Set Methods

Duplicate inserts are silently ignored. Iterate via .to_array():

for x in s.to_array() {
    print(x)
}

std.collections

Functional operations on arrays. Import with import std.collections.

import std.collections

fn main() {
    let nums = [1, 2, 3, 4, 5]
    let doubled = collections.map(nums, (x: int) => x * 2)
    let evens = collections.filter(nums, (x: int) => x % 2 == 0)
    let total = collections.fold(nums, 0, (acc: int, x: int) => acc + x)
}

Function Reference

zip and enumerate return Pair<A, B> (from std.collections) with fields first and second:

import std.collections

fn main() {
    let pairs = collections.enumerate(["alice", "bob"])
    for p in pairs {
        print(f"{p.first}: {p.second}")  // 0: alice, 1: bob
    }
}

Data Modeling

Pluto has three data modeling primitives: classes, traits, and enums. There is no inheritance. Composition happens through dependency injection and embedding. Polymorphism happens through traits. This is intentional.

Classes model values — data, compared by content. For things with identity — services, resources, shared state — Pluto has a fourth construct, object, covered in Objects and Entities. This chapter is about values.

Classes

A class is a named collection of fields with methods.

class Point {
    x: float
    y: float

    fn distance(self, other: Point) float {
        let dx = self.x - other.x
        let dy = self.y - other.y
        return dx * dx + dy * dy
    }

    fn translate(self, dx: float, dy: float) Point {
        return Point { x: self.x + dx, y: self.y + dy }
    }
}

Instantiate with struct literal syntax. Methods require self as the first parameter:

let p = Point { x: 1.0, y: 2.0 }
let q = p.translate(3.0, 4.0)
print(p.distance(q))

Equality Is Structural

Values are their content, and == says so. Two class instances with equal fields are equal, recursively — through nested classes, enums, arrays, maps, sets, and nullables (maps and sets compare order-independently):

class Address { city: string }
class Person { name: string, address: Address }

fn main() {
    let a = Person { name: "alice", address: Address { city: "nyc" } }
    let b = Person { name: "alice", address: Address { city: "nyc" } }
    print(a == b)    // true — same content, same value
}

This is the rule for every value shape in the language. The one thing compared by identity inside a structural comparison is an entity (object) — equal state in a different entity is still a different entity.

Mutation

Use mut self to declare a method that mutates fields:

class Counter {
    val: int

    fn increment(mut self) {
        self.val = self.val + 1
    }
}

The compiler enforces mutability: only mut self methods can assign to self.field, and callers must hold a mutable reference to call mut self methods on an object.

Composition and Chaining

Classes contain other classes as fields – this is how you compose, not through inheritance:

class Address { city: string }
class Person { name: string, address: Address }

fn main() {
    let p = Person { name: "alice", address: Address { city: "new york" } }
    print(p.address.city)
}

Methods returning the same class type can be chained:

class Builder {
    val: int
    fn add(self, n: int) Builder { return Builder { val: self.val + n } }
}

fn main() {
    let result = Builder { val: 0 }.add(1).add(2).add(3)
    print(result.val)    // 6
}

Traits

Traits define shared behavior. They are Pluto’s mechanism for polymorphism.

Definition and Implementation

trait HasArea {
    fn area(self) int
}

class Circle impl HasArea {
    radius: int
    fn area(self) int { return 3 * self.radius * self.radius }
}

class Square impl HasArea {
    side: int
    fn area(self) int { return self.side * self.side }
}

impl goes on the class declaration. A class can implement multiple traits:

class Point impl HasX, HasY {
    x: int
    y: int
    fn get_x(self) int { return self.x }
    fn get_y(self) int { return self.y }
}

The compiler verifies that all required methods are present with correct signatures.

Structural Typing

Traits use structural typing. If a class has the right methods, it satisfies the trait – even without an explicit impl. The impl keyword is documentation and compile-time verification, not a requirement for dispatch.

Default Methods

Traits can provide default implementations that classes inherit or override:

trait Greetable {
    fn greet(self) string { return "hello" }
}

class User impl Greetable { name: string }

class Admin impl Greetable {
    name: string
    fn greet(self) string { return f"hello, admin {self.name}" }
}

Trait-Typed Parameters

Use a trait as a parameter type for polymorphic dispatch:

fn print_area(shape: HasArea) {
    print(shape.area())
}

fn main() {
    print_area(Circle { radius: 5 })
    print_area(Square { side: 4 })
}

This uses vtable-based dynamic dispatch. You can also declare variables with trait types: let shape: HasArea = Circle { radius: 5 }.

Traits with Contracts

Trait methods can carry requires clauses, enforced at runtime on all implementors:

trait Validator {
    fn validate(self, x: int) int
        requires x > 0
}

class Doubler impl Validator {
    id: int
    fn validate(self, x: int) int { return x * 2 }
}

Calling validate(-1) aborts with a requires violation. Implementations cannot add requires of their own — demanding more than the trait promised would break substitutability (Liskov substitution principle), and the compiler rejects it. See Contracts.

Enums

Enums represent a type that is one of several variants.

Unit and Data-Carrying Variants

enum Color { Red, Green, Blue }

enum Shape {
    Circle { radius: float }
    Rect { w: float, h: float }
}

let c = Color.Red
let s = Shape.Circle { radius: 3.14 }

You can mix unit and data variants in the same enum.

Pattern Matching

Use match to destructure enums. Data variant bindings go in the first { }, the arm body in the second:

fn describe(s: Shape) {
    match s {
        Shape.Circle { radius } {
            print(f"circle r={radius}")
        }
        Shape.Rect { w, h } {
            print(f"rect {w}x{h}")
        }
    }
}

Unit variants have no bindings – just the body block:

match c {
    Color.Red { print("red") }
    Color.Green { print("green") }
    Color.Blue { print("blue") }
}

Exhaustiveness Checking

The compiler rejects non-exhaustive matches. Miss a variant, get a compile error.

Enums as Parameters and Return Types

enum Result {
    Ok { value: int }
    Err { code: int }
}

fn compute(x: int) Result {
    if x > 0 {
        return Result.Ok { value: x * 2 }
    }
    return Result.Err { code: -1 }
}

fn main() {
    let r = compute(5)
    match r {
        Result.Ok { value } { print(value) }
        Result.Err { code } { print(code) }
    }
}

The Design Philosophy

No inheritance. This is the most important design decision in Pluto’s type system. Behavior reuse happens through dependency injection (class UserService[db: Database]). Polymorphism happens through traits. Data composition happens through embedding.

There is no extends, no super, no method resolution order, no diamond problem, no fragile base class problem. The language does not have these concepts, and the programs are simpler for it.

Closures and Generics

Closures

Closures are anonymous functions that capture variables from their enclosing scope.

Syntax

Arrow syntax: (params) => expression or (params) => { block }.

let double = (x: int) => x * 2
let greet = () => "hello"
let add = (a: int, b: int) => a + b

For multi-statement bodies, use a block with explicit return:

let classify = (x: int) => {
    if x > 0 {
        return "positive"
    }
    return "non-positive"
}

Function Types

The type of a closure is fn(param_types) return_type:

Capture by Value

Closures capture a snapshot at creation time:

fn main() {
    let mut a = 10
    let f = (x: int) => x + a
    print(f(5))    // 15
    a = 999
    print(f(5))    // still 15
}

Primitives (int, float, bool) are copied. Heap types (strings, classes, arrays) share the underlying data – the pointer is copied, not the object.

Higher-Order Functions

Functions accept closures as parameters and can return them:

fn apply(f: fn(int) int, x: int) int {
    return f(x)
}

fn make_adder(n: int) fn(int) int {
    return (x: int) => x + n
}

fn main() {
    print(apply((x: int) => x * 3, 7))    // 21

    let add5 = make_adder(5)
    print(add5(3))    // 8
}

Closures in Arrays

fn main() {
    let ops: [fn(int) int] = [
        (x: int) => x + 1,
        (x: int) => x * 2,
        (x: int) => x * x
    ]
    for op in ops {
        print(op(5))
    }
}

Generics

Generics let you write functions, classes, and enums that work with any type. Pluto uses monomorphization: the compiler generates a specialized copy for each concrete type, like Rust. Zero runtime overhead.

Generic Functions

Type parameters go in angle brackets after the function name:

fn identity<T>(x: T) T {
    return x
}

fn main() {
    print(identity(42))        // 42
    print(identity("hello"))   // hello
}

Type arguments are usually inferred from usage. You can also specify them explicitly: identity<int>(42).

Multiple Type Parameters

fn first<A, B>(a: A, b: B) A {
    return a
}

print(first(1, "hello"))    // 1

Generic Classes

Classes can have type parameters. Specify the concrete type when constructing:

class Box<T> {
    value: T

    fn get(self) T {
        return self.value
    }
}

fn main() {
    let b = Box<int> { value: 42 }
    print(b.get())    // 42

    let s = Box<string> { value: "hello" }
    print(s.get())    // hello
}

Multiple type parameters:

class Pair<A, B> {
    first: A
    second: B
}

let p = Pair<string, int> { first: "age", second: 25 }

Generic Enums

enum Result<T> {
    Ok { value: T }
    Err { message: string }
}

fn divide(a: int, b: int) Result<int> {
    if b == 0 {
        return Result<int>.Err { message: "division by zero" }
    }
    return Result<int>.Ok { value: a / b }
}

fn main() {
    let r = divide(10, 3)
    match r {
        Result.Ok { value } { print(value) }
        Result.Err { message } { print(message) }
    }
}

How Monomorphization Works

Box<int> and Box<string> become completely separate types at compile time. No type erasure, no boxing, no vtable overhead. Generic code is as fast as hand-written specialized code, at the cost of binary size when many instantiations exist.

Type Bounds

You can constrain type parameters to types that implement one or more traits:

fn print_area<T: HasArea>(shape: T) {
    print(shape.area())
}

fn process<T: Readable + Writable>(item: T) {
    let data = item.read()
    item.write(data)
}

The compiler validates bounds at every instantiation site.

Explicit Type Arguments

Type arguments are usually inferred, but you can specify them explicitly:

let x = identity<int>(42)

Generic Classes with Traits

Generic classes can implement traits. The compiler validates method signatures after monomorphization:

class Box<T> impl Printable {
    value: T
    fn to_string(self) string { return "Box" }
}

Generic DI

Classes with bracket deps can have type parameters:

class Repository<T>[db: Database] {
    fn find(self, id: int) T {
        return self.db.query(f"SELECT * WHERE id = {id}")!
    }
}

Nullable Types

Every mainstream language has gotten null wrong at least once.

Go has nil. Any pointer, interface, slice, map, or channel can be nil. The compiler does not help – a nil dereference is a runtime panic.

Java has null. Any reference type can be null at any time. NullPointerException is the most common crash in Java’s history. Kotlin fixed this with String? vs String, but it required a new language.

Rust has Option<T>. Correct, but ceremonious. Every nullable value needs Option<T>, every access needs match or if let Some(x) or .map(). Safety at the cost of verbosity.

Pluto treats nullability as a first-class type modifier: compiler-enforced, minimal syntax.

T?, none, and Nullable Returns

Any type becomes nullable by appending ?. The literal none represents absence:

let x: int? = none
let name: string? = "Alice"
let p: Point? = Point { x: 1, y: 2 }

Functions declare nullable return types with T?. Returning a concrete T coerces implicitly to T?:

fn find_positive(x: int) int? {
    if x > 0 {
        return x
    }
    return none
}

The ? Operator

The ? postfix operator unwraps a nullable. If none, it early-returns none from the enclosing function:

fn double_it() int? {
    let x = get_value()?    // returns none if get_value() returned none
    return x * 2
}

This mirrors how ! works for error propagation. Multiple ? calls chain with short-circuit semantics:

fn pipeline() int? {
    let a = step1()?       // returns none if step1 returned none
    let b = step2(a)?      // returns none if step2 returned none
    return b
}

When step1() returns none, step2 is never called.

? in Void Functions

In void functions, ? acts as an early return instead of returning none:

fn process(line: string?) {
    let value = line?      // if none, return from process()
    print(value)
}

fn main() {
    process("hello")       // prints "hello"
    process(none)           // silently returns
    print("done")          // prints "done"
}

Coercion Rules

T is assignable to T? (implicit wrap). T? is NOT assignable to T – you must unwrap with ?:

fn takes_int(x: int) { }

fn main() int? {
    let x: int? = 42
    takes_int(x)            // COMPILE ERROR: int? is not int
    takes_int(x?)           // OK: unwraps or early-returns none
    return none
}

This applies uniformly to parameters, classes, and all other types:

fn unwrap_it(x: int?) int? {
    let val = x?
    return val + 1
}

fn maybe_point() Point? {
    return Point { x: 1, y: 2 }
}

fn use_it() int? {
    let p = maybe_point()?
    return p.x + p.y
}

String Parsing

The built-in to_int() and to_float() return nullable types rather than raising errors:

let n = "42".to_int()       // int?
let f = "3.14".to_float()   // float?
let bad = "abc".to_int()    // int? (none)

Restrictions

• No nested nullables. int?? is a compile error.
• No void?. Void cannot be nullable.
• ? requires a nullable operand. Using ? on a non-nullable is a compile error.
• ? requires a compatible return type. The enclosing function must return T? or void.

Comparison

Pluto’s nullable types give you Kotlin’s ergonomics with Rust’s safety guarantees, without the ceremony of Option<T> and match.

Modules and Packages

Pluto has two levels of code organization: modules for splitting code across files, and packages for managing external dependencies.

Modules

Importing a Module

The import keyword loads a module by name. All access is qualified:

import math

fn main() {
    print(math.add(1, 2))
}

There are no unqualified imports, no from X import Y, no glob imports.

Single-File and Directory Modules

import math looks for math.pluto or a math/ directory next to your entry file.

A single-file module is just a .pluto file. A directory module merges all .pluto files within it into a single namespace – files in the directory see each other without explicit imports.

Visibility

Declarations are private by default. Use pub to export:

fn helper(x: int) int { return x * 2 }        // private

pub fn double(x: int) int { return helper(x) } // public

pub applies to fn, class, trait, and enum.

Qualified Access

Importers use qualified names for everything – functions, classes, enums, types in signatures:

import geo

fn show(p: geo.Point) {
    print(p.sum())
}

fn main() {
    let p = geo.Point { x: 10, y: 20 }
    show(p)

    let s = status.State.Active
    match s {
        status.State.Active { print("active") }
        status.State.Inactive { print("inactive") }
    }
}

Hierarchical Imports and Aliases

Modules nest in subdirectories via dot syntax. The binding name is the last segment:

import utils.math          // resolves utils/math.pluto or utils/math/
                           // bound as: math.add(...)

import a.b.c               // resolves a/b/c.pluto or a/b/c/
                           // bound as: c.whatever()

import math as m           // alias: m.add(...)

Same-Directory Auto-Merge

Files in the same directory as your entry file are automatically merged without imports:

// main.pluto                    // helper.pluto (same directory)
fn main() {                      fn helper() int {
    print(helper())                  return 99
}                                }

Standard Library

Standard library modules use the std namespace:

import std.strings
import std.math
import std.collections

Use --stdlib stdlib to point the compiler at the stdlib directory, or place a stdlib/ directory next to your entry file.

Transitive and Circular Imports

Modules can import other modules transitively. If shapes imports geo, and you import shapes, everything resolves. Circular imports are detected and rejected at compile time.

Packages

Modules organize code within a project. Packages handle external dependencies via pluto.toml.

pluto.toml

[package]
name = "myapp"
version = "0.1.0"

[dependencies]
mathlib = { path = "deps/mathlib" }

The compiler walks up from your entry file looking for pluto.toml (stopping at .git boundaries). Projects without a manifest work exactly as before.

Path Dependencies

[dependencies]
mathlib = { path = "deps/mathlib" }
utils = { path = "../shared/utils" }

Paths are relative to pluto.toml. Import by the dependency name, not the directory name:

import mathlib

fn main() {
    print(mathlib.add(1, 2))
}

Git Dependencies

[dependencies]
strutils = { git = "https://github.com/user/strutils.git" }
mylib = { git = "https://github.com/user/mylib.git", tag = "v1.0" }
pinned = { git = "https://github.com/user/lib.git", rev = "abc123f" }
latest = { git = "https://github.com/user/lib.git", branch = "dev" }

Specify at most one of rev, tag, or branch. Repos are cached in ~/.pluto/cache/git/. Run pluto update to re-fetch.

A Complete Example

myapp/
  pluto.toml
  main.pluto
  deps/
    mathlib/
      add.pluto
      mul.pluto

pluto.toml:

[package]
name = "myapp"
version = "0.1.0"

[dependencies]
mathlib = { path = "deps/mathlib" }

deps/mathlib/add.pluto:

pub fn add(a: int, b: int) int {
    return a + b
}

main.pluto:

import mathlib

fn main() {
    print(mathlib.add(1, 2))
}

Transitive Dependencies

Packages can declare their own pluto.toml with their own dependencies:

# deps/liba/pluto.toml
[package]
name = "liba"

[dependencies]
libb = { path = "../../deps/libb" }

// deps/liba/compute.pluto
import libb

pub fn compute(x: int) int {
    return libb.double(x)
}

The compiler resolves the full graph, deduplicates diamonds, and detects circular chains.

Scope Isolation

Transitive dependencies are not visible unless explicitly declared. If you depend on liba and liba depends on libb, you cannot import libb without adding it to your own pluto.toml. This prevents coupling to implementation details of your dependencies.

Rules and Constraints

Naming: Dependency names must be valid identifiers. std and language keywords (class, fn, if, etc.) are reserved.

Collisions: If a dependency name matches a local module directory, the compiler reports an ambiguity error.

Mixing: Path and git dependencies work together in the same manifest.

Summary

Testing

Pluto has a built-in test framework. No test runner to install, no assertion library to import, no special project structure. Tests live next to the code they test.

Test Blocks

A test is a named block:

test "name" {
    // test body
}

Tests can appear anywhere in a file, alongside functions, classes, and other declarations. Multiple tests per file is normal and expected:

fn factorial(n: int) int {
    if n <= 1 { return 1 }
    return n * factorial(n - 1)
}

test "factorial base case" {
    expect(factorial(0)).to_equal(1)
    expect(factorial(1)).to_equal(1)
}

test "factorial recursive" {
    expect(factorial(5)).to_equal(120)
    expect(factorial(10)).to_equal(3628800)
}

Running Tests

$ pluto test main.pluto

The compiler compiles the file in test mode, which generates a test runner as the entry point. Each test block runs in sequence, and the runner reports pass/fail for each.

Under normal compilation (pluto compile or pluto run), test blocks are stripped entirely. They contribute zero overhead to the production binary.

Assertions

The assertion API is expect(value) followed by a matcher:

• expect(x).to_equal(y) – asserts x == y. Works with int, float, bool, string.
• expect(b).to_be_true() – asserts b is true.
• expect(b).to_be_false() – asserts b is false.

A failed assertion reports the test name, expected value, and actual value, then marks the test as failed.

fn clamp(x: int, lo: int, hi: int) int {
    if x < lo { return lo }
    if x > hi { return hi }
    return x
}

test "clamp within range" {
    expect(clamp(5, 0, 10)).to_equal(5)
}

test "clamp below minimum" {
    expect(clamp(-3, 0, 10)).to_equal(0)
}

test "clamp above maximum" {
    expect(clamp(15, 0, 10)).to_equal(10)
}

Testing Error-Raising Code

expect_raises asserts that a block raises an error of a specific type:

error InvalidInput {
    message: string
}

fn parse_positive(n: int) int {
    if n <= 0 {
        raise InvalidInput { message: "must be positive" }
    }
    return n
}

test "parse_positive succeeds" {
    let result = parse_positive(5) catch -1
    expect(result).to_equal(5)
}

test "parse_positive rejects zero" {
    expect_raises(InvalidInput) {
        parse_positive(0)!
    }
}

Inside the block, ! propagates to the construct itself — the enclosing test does not become fallible. The assertion fails if the block completes without raising (expected InvalidInput to be raised, but no error was raised) or raises a different error type (expected InvalidInput to be raised, got SegmentError); either way the error is consumed by the construct and does not escape the test. A wildcard form asserts that the block raises something, whatever the type:

test "parse_positive rejects negatives" {
    expect_raises {
        parse_positive(-3)!
    }
}

The assertion is checked against the compiler’s inferred error sets at compile time. A block that cannot raise at all is a compile error (expect_raises block cannot raise), and naming an error type the block cannot produce is one too (the block can raise 'InvalidInput' — not 'IoError'), so an error-path test can never silently pass for the wrong reason.

expect_raises asserts on the error type only. To inspect an error’s fields, use catch — it handles the error inline, exactly as it does in production code:

test "error carries the message" {
    let mut seen = ""
    let v = parse_positive(0) catch err: InvalidInput {
        seen = err.message
        0
    }
    expect(v).to_equal(0)
    expect(seen).to_equal("must be positive")
}

Tests in Modules

Tests defined in imported modules are private. They are not exported, not visible to the importing file, and not run when the importing file is tested. Only tests in the file passed to pluto test are executed.

This means each module can have its own test suite, run independently:

$ pluto test lib.pluto       # runs tests in lib.pluto
$ pluto test main.pluto      # runs tests in main.pluto (not lib.pluto's tests)

Testing Concurrent Code

Tests that use spawn, channels, or select run under a deterministic test scheduler with four strategies — including an exhaustive mode that runs every meaningfully distinct interleaving. By default, spawned tasks run inline, so tests where tasks coordinate with each other need a tests[scheduler: ...] block:

tests[scheduler: Exhaustive] {
    test "producer and consumer" {
        // spawn + channel coordination works here
    }
}

See Testing Concurrent Code for the strategies, when you need each one, and how to read the scheduler’s deadlock reports.

Testing Concurrent Code

Tests that use spawn, channels, or select run under a deterministic test scheduler. In test mode there are no OS threads: spawned tasks become cooperative fibers, and the scheduler decides exactly which task runs at every blocking point. The same test run always executes the same way — concurrency bugs reproduce instead of flaking.

The scheduler has four strategies. Which one a test file uses is chosen with a tests block:

tests[scheduler: Exhaustive] {
    test "name" {
        // test body
    }
}

A file can have at most one tests block, and its strategy applies to every test in the file (including bare test blocks outside it). Without a tests block, tests run under Sequential.

The Four Strategies

Sequential

The default. A spawned task runs immediately and completely at the spawn expression, as if it were a plain function call. This is fast and perfectly deterministic, and it is all you need when tasks don’t coordinate with each other:

fn add(a: int, b: int) int {
    return a + b
}

test "spawn returns result" {
    let t = spawn add(1, 2)
    expect(t.get()).to_equal(3)
}

What Sequential cannot do is interleave. If a spawned task has to wait for something the test body does later, there is nothing to resume it — the task runs before the test body continues. That is the one failure mode to know about, covered in the next section.

RoundRobin

The cheapest strategy with real concurrency. Every task is a fiber; whenever a fiber blocks (channel send/recv, select, task.get()), the scheduler hands control to the next ready fiber in creation order. Coordinating tasks make progress together, and the interleaving is still fully deterministic:

fn pong(ping_rx: Receiver<int>, pong_tx: Sender<int>) {
    let v = ping_rx.recv()!
    pong_tx.send(v + 1)!
}

tests[scheduler: RoundRobin] {
    test "ping pong" {
        let (ping_tx, ping_rx) = chan<int>(1)
        let (pong_tx, pong_rx) = chan<int>(1)
        let t = spawn pong(ping_rx, pong_tx)
        ping_tx.send(1)!
        expect(pong_rx.recv()!).to_equal(2)
        t.get()!
    }
}

RoundRobin checks that your code works under one concurrent schedule. It will not find bugs that only appear under a different ordering.

Random

Like RoundRobin, but at each blocking point the scheduler picks a random ready fiber, and the whole test is run 100 times with different seeds. Good for shaking out ordering assumptions cheaply:

tests[scheduler: Random] {
    test "transfer completes under random schedules" {
        ...
    }
}

When a run fails, the runner prints the seed and iteration so the exact schedule can be replayed. Two environment variables control the sampling: PLUTO_TEST_SEED fixes the base seed, PLUTO_TEST_ITERATIONS changes the run count.

Exhaustive

The strongest strategy: the test is run repeatedly, once per meaningfully distinct interleaving, until the entire schedule space is covered — and every interleaving must pass. Naively there are exponentially many schedules, so the scheduler uses dynamic partial order reduction (DPOR): two schedules that differ only in the order of operations that cannot affect each other (different channels, no shared state) produce the same result, so only one of them is run. What remains is every ordering that could actually change behavior.

fn produce(tx: Sender<int>, value: int) {
    tx.send(value)!
}

tests[scheduler: Exhaustive] {
    test "two producers race" {
        let (tx, rx) = chan<int>(2)
        let a = spawn produce(tx, 1)
        let b = spawn produce(tx, 2)
        let first = rx.recv()!
        let second = rx.recv()!
        a.get()!
        b.get()!
        expect(first + second).to_equal(3)
    }
}

The two producers race to send first, so first could be 1 or 2 — the assertion only checks the order-independent sum. The runner reports its coverage of the schedule space:

test two producers race ...   Exhaustive: 4 schedules explored
ok

If an assertion fails or a deadlock exists in any interleaving, Exhaustive finds it and reports which schedule triggered it. Exploration is capped at 10,000 schedules by default; PLUTO_MAX_SCHEDULES and PLUTO_MAX_DEPTH adjust the limits for very large tests.

“Blocked … in Sequential Test Mode”

The first concurrent test most people write looks like this: spawn a worker, send it a request, read its reply.

fn worker(requests: Receiver<int>, replies: Sender<int>) {
    let n = requests.recv()!
    replies.send(n * 2)!
}

test "worker doubles" {
    let (req_tx, req_rx) = chan<int>(1)
    let (rep_tx, rep_rx) = chan<int>(1)
    let t = spawn worker(req_rx, rep_tx)
    req_tx.send(21)!
    expect(rep_rx.recv()!).to_equal(42)
    t.get()!
}

This code is correct under concurrent execution — and it aborts under the default scheduler:

pluto: blocked channel recv on empty buffer in sequential test mode — spawned
tasks run inline, so coordinating tasks cannot interleave. If this code is
correct under concurrency, run it under the exploration scheduler:
tests[scheduler: Exhaustive] { ... }. Strategies: Sequential (default),
RoundRobin, Random, Exhaustive.

Decoding it: under Sequential, the worker runs inline, at the spawn site, before req_tx.send(21)! ever executes. It calls requests.recv() on a still-empty channel, and no other task can run to fill it — so the scheduler stops. This is a property of the sequential strategy, not a verdict on your program. The same message appears as blocked channel send on full buffer (a task sends into a channel nothing has drained yet) and blocked select with no ready channels (no arm can proceed and there is no default).

The fix is in the message: if the code is supposed to work because tasks interleave, run it under a scheduler that interleaves them. Wrap the tests in a block:

tests[scheduler: Exhaustive] {
    test "worker doubles" {
        let (req_tx, req_rx) = chan<int>(1)
        let (rep_tx, rep_rx) = chan<int>(1)
        let t = spawn worker(req_rx, rep_tx)
        req_tx.send(21)!
        expect(rep_rx.recv()!).to_equal(42)
        t.get()!
    }
}

Now the worker fiber blocks on recv, the test body resumes and sends, the worker wakes — and Exhaustive proves the test passes under every distinct ordering.

Rule of thumb: the moment a test spawns a task that communicates with the test body (or with other tasks) through channels or select, put it under tests[scheduler: Exhaustive]. Use RoundRobin when you only want one deterministic concurrent schedule, and Random for cheap broad sampling of bigger tests where exhaustive exploration is too slow.

Real Deadlocks

Under the exploration schedulers, a deadlock report means the real thing: an interleaving exists in which every task is blocked and none can ever proceed. The runner shows what each fiber was waiting on, and under Exhaustive, which schedule reached the deadlock:

pluto: deadlock detected in test
  Fiber 0: blocked on task.get()
  Fiber 1: blocked on chan.recv()
  Fiber 2: blocked on chan.recv()
  Exhaustive: 1 schedule explored
  1 failure found:
    - deadlock in schedule 0 (depth 3)

Fiber 0 is the test body itself; fibers are numbered in spawn order. Here two workers each wait to receive from a channel only the other would fill — a circular wait that no schedule can resolve. Unlike the sequential-mode abort above, this one is telling you about a bug in the program.

Testing a select

select works under all strategies, but it is most at home under Exhaustive, which explores each arm-readiness ordering that can occur:

fn echo(inbox: Receiver<int>, outbox: Sender<int>) {
    let v = inbox.recv()!
    outbox.send(v + 1)!
}

tests[scheduler: Exhaustive] {
    test "select hears whichever worker answers" {
        let (a_tx, a_rx) = chan<int>(1)
        let (b_tx, b_rx) = chan<int>(1)
        let (out_tx, out_rx) = chan<int>(2)
        let a = spawn echo(a_rx, out_tx)
        let b = spawn echo(b_rx, out_tx)
        a_tx.send(10)!
        b_tx.send(20)!
        let mut total = 0
        let mut seen = 0
        while seen < 2 {
            select {
                v = out_rx.recv() {
                    total = total + v
                    seen = seen + 1
                }
            }
        }
        a.get()!
        b.get()!
        expect(total).to_equal(32)
    }
}

Either worker may answer first; the test asserts only what must hold in every ordering. Exhaustive then runs all distinct orderings and confirms it.

Pinning a Failure as a Regression Test

Every test run records its scheduling decisions. When anything fails — an expect, a deadlock, an exhaustive-found interleaving — the runner prints a repro block:

FAIL (line 19): expected 2 to equal 1
  strategy: Random  seed: 0x3  iteration: 1
  schedule: ptsched:v1:AQABAgEAAQEBAA==
  rerun:    pluto test <file> --test "transfer" --schedule ptsched:v1:AQABAgEAAQEBAA==

The rerun: line reproduces the failure immediately. To keep it reproduced forever, copy the pin into the test header:

tests[scheduler: Random, seed: 7, iterations: 1000] {
    // Re-runs exactly that random iteration:
    test "regression: lost transfer, #512" [seed: 3, iteration: 1] { ... }

    // Or replays the recorded interleaving decision by decision:
    test "regression: lost transfer, #512" [schedule: "ptsched:v1:AQABAgEAAQEBAA=="] { ... }
}

A seed pin is compact and survives unrelated refactors; a schedule pin is exact and is the only repro form for failures found by Exhaustive (no seed generates a DPOR schedule). A replayed schedule that no longer matches the code’s concurrency structure fails loudly rather than silently passing — re-record it with --until-failure and update the pin.

The block header also takes seed: and iterations: to fix Random’s sampling in source, and the CLI can override everything:

pluto test file.pt --test "one test"             # filter to one test
pluto test file.pt --strategy Exhaustive         # override the block strategy
pluto test file.pt --seed 0x3                    # hex seeds, as printed
pluto test file.pt --test "t" --until-failure    # hunt seeds until a failure, print its pin
pluto test file.pt --test "t" --schedule ptsched:v1:...   # replay a token

CLI flags beat in-source pins, so a stale pin can be re-hunted without editing the file.

AI-Native Development

Whole-program compilation means the Pluto compiler builds a complete understanding of your program: resolved types for every expression, inferred error sets for every function, the full call graph, the dependency wiring topology, cross-references between every declaration and its usage sites.

Most compilers throw this knowledge away after code generation. Pluto keeps it.

The compiler’s internal representation — the AST, the type information, the analysis results — is a first-class artifact: serializable, queryable, and designed for AI agents to read and write directly. The compiler sees your entire program and understands it deeply. AI agents get access to that same understanding through a structured API.

This chapter covers what is implemented today and where the design is headed.

What Exists Now

Binary AST Format (PLTO)

Pluto source files can be compiled to a binary AST format that preserves the full semantic graph:

$ pluto emit-ast main.pt -o main.pluto       # text -> binary AST
$ pluto generate-pt main.pluto                # binary AST -> text (stdout)
$ pluto generate-pt main.pluto -o main.pt     # binary AST -> text file
$ pluto sync main.pt --output main.pluto      # merge text edits back, preserving UUIDs

The binary format (.pluto) contains the complete parsed AST, the original source text, and derived analysis data. The text format (.pt) is standard Pluto syntax that humans read and edit.

Stable UUIDs

Every declaration in a Pluto program has a stable UUID: functions, classes, enums, traits, methods, fields, parameters, error declarations, enum variants, and app declarations. UUIDs are assigned at creation time and survive renames, moves, and refactors.

This is the foundation. When an AI agent renames a function, the UUID stays the same. Every call site, struct literal, enum usage, and raise site that references that declaration tracks the UUID, not the name string. The name is display text. The UUID is identity.

Cross-References

The compiler resolves and stores cross-references by UUID:

• Call sites – which functions call which other functions, tracked by the callee’s UUID
• Struct literals – where each class is constructed, tracked by the class UUID
• Enum usages – where each enum variant is used, tracked by enum and variant UUIDs
• Raise sites – where each error type is raised, tracked by the error UUID

These are not heuristics or text search. They are exact, compiler-resolved references that survive across renames.

The SDK (pluto-sdk)

The SDK is a Rust crate for reading and writing Pluto programs as structured data. It is what AI agents (and any tooling) use to interact with Pluto code without parsing text.

Loading a module:

#![allow(unused)]
fn main() {
use pluto_sdk::Module;

// From binary format
let module = Module::from_bytes(&bytes)?;

// From source text (parse without full compilation)
let module = Module::from_source(source)?;

// From a .pluto source file (full front-end pipeline with analysis)
let module = Module::from_source_file("main.pluto")?;
}

Querying:

#![allow(unused)]
fn main() {
// List all functions, classes, enums, traits, errors
for f in module.functions() {
    println!("{}: {}", f.name(), f.id());
}

// Look up by name or UUID
let decls = module.find("process_order");
let decl = module.get(some_uuid);

// Cross-references
let callers = module.callers_of(function_uuid);
let constructors = module.constructors_of(class_uuid);
let usages = module.enum_usages_of(enum_uuid);
let raises = module.raise_sites_of(error_uuid);
}

Editing:

#![allow(unused)]
fn main() {
let mut editor = module.edit();

// Add declarations
let id = editor.add_from_source("fn greet() {\n    print(\"hello\")\n}\n")?;

// Replace (preserves UUID)
editor.replace_from_source(existing_id, "fn greet() {\n    print(\"goodbye\")\n}\n")?;

// Rename (updates all references)
editor.rename(function_id, "hello")?;

// Add methods and fields to classes
editor.add_method_from_source(class_id, "fn area(self) float {\n    return self.w * self.h\n}\n")?;
editor.add_field(class_id, "z", "float")?;

// Delete (reports dangling references)
let result = editor.delete(function_id)?;
for d in &result.dangling {
    eprintln!("warning: dangling reference to '{}' at {:?}", d.name, d.span);
}

// Commit: re-serializes source, rebuilds index and xrefs
let module = editor.commit();
}

The key property: edits are UUID-stable. Renaming a function updates the declaration’s name and every reference site in a single operation. The UUID never changes.

The MCP Server

The MCP (Model Context Protocol) server exposes the SDK’s capabilities as structured tools that AI agents call directly. This is how Claude, and other LLM-based agents, interact with Pluto codebases.

Read tools:

Write tools:

Build tools:

The agent workflow is: load a module, query its structure, understand types and error sets, make a targeted edit, validate with the type checker, iterate.

The Vision: Programs, Not Services

The tools above are implemented and working. The larger vision takes them further — toward a world where distributed systems are programs, not collections of services.

The Four Pillars

1. Whole-program compilation. The compiler sees your entire distributed system: every stage, every function call, every error that could be raised. It generates per-stage binaries with all RPC code.

2. Source-level composition. There are no library binaries, no ABI boundaries. All dependencies are source code. The compiler integrates them into your program and optimizes across module boundaries.

3. Stages as deployment units. You declare stage api, stage workers, stage analytics in your program. The compiler knows which calls cross stage boundaries and generates the RPC code.

4. AI agents as first-class developers. The compiler’s internal representation (AST, types, call graph, error sets) is a queryable artifact. AI agents read and write programs at the semantic level, not as text.

When these four pillars are complete, you’ll write a Pluto program that defines your entire backend — all services, all communication, all schemas — and the compiler will generate deployable binaries, migration scripts, API documentation, and monitoring hooks automatically.

You write logic. The compiler generates infrastructure.

The Vision

.pluto as Canonical Source

Today, .pt text files are the source of truth and .pluto binary files are derived. The plan is to invert this: .pluto binary becomes canonical, .pt text files become generated views for human review.

In this model, a git repository contains .pluto binaries (committed, source of truth) and .pt text files (generated, for review and code search). The pluto sync command already exists to merge human .pt edits back into .pluto files, preserving UUIDs where declarations match by name.

Derived Data

The compiler produces valuable analysis that is currently discarded after each build: resolved types for every expression, inferred error sets, the full call graph, DI wiring topology. The derived data layer stores this analysis in the .pluto binary so that agents and tools can query it without re-compiling.

The SDK already surfaces derived data (resolved signatures, class info, enum info, error info) when a module is loaded via from_source_file. The plan is to extend this to the full set of compiler analysis.

The Feedback Loop

The core idea is that the compiler and AI agents form a feedback loop:

1. Agent writes code – using the SDK or MCP server, the agent makes structured edits with stable UUIDs.
2. Compiler analyzes – type checking, error inference, call graph construction. The analysis is stored, not discarded.
3. Agent reads analysis – the agent queries resolved types, error sets, cross-references. It learns what the compiler knows about the code.
4. Agent writes better code – informed by the compiler’s analysis, the agent makes its next edit with full knowledge of the type system, error propagation, and dependency graph.

This is not AI replacing developers. It is the compiler’s understanding of your program being accessible to every tool in the chain – AI agents, editors, code review systems, refactoring tools – through a structured interface with stable identities.

The text file is a view. The semantic graph is the source.

What This Looks Like in Practice

Imagine building a production backend in 2027 with Pluto. Here’s what the workflow looks like:

You Write One Program

// main.pluto
stage api[db: Database] {
    fn handle_order(req: OrderRequest) OrderResponse {
        let user = auth.verify_user(req.token)!
        let inventory = warehouse.check_stock(req.items)!
        let order = self.db.create_order(user.id, req.items)!
        payments.charge_async(order.id, order.total)
        return OrderResponse { order_id: order.id }
    }
}

stage auth {
    pub fn verify_user(token: string) User {
        // JWT validation
    }
}

stage warehouse {
    pub fn check_stock(items: Array<Item>) Inventory {
        // inventory lookup
    }
}

stage payments {
    pub fn charge_async(order_id: string, amount: int) {
        // async payment processing
    }
}

This is your entire backend. Four stages, defined in one program.

The Compiler Sees Everything

When you run pluto compile main.pluto, the compiler:

1. Parses and type-checks all four stages together
2. Infers error sets — sees that verify_user can raise InvalidToken, check_stock can raise OutOfStock, create_order can raise DatabaseError
3. Analyzes call graph — sees that api calls auth, warehouse, and payments across stage boundaries
4. Generates RPC code — serialization for OrderRequest, User, Item, Inventory; HTTP client calls; error propagation for both remote errors and network failures
5. Generates per-stage binaries — build/api, build/auth, build/warehouse, build/payments

An AI Agent Adds a Feature

You ask Claude: “Add fraud detection before charging payments.”

Claude uses the MCP server to:

1. Load the program — load_module("main.pluto")
2. Query the structure — list_declarations() shows all four stages and their functions
3. Inspect the payments stage — inspect("payments.charge_async") shows params, return type, error set
4. Add a new stage:

stage fraud {
    error FraudDetected { order_id: string, reason: string }

    pub fn check_order(order_id: string, amount: int) {
        if amount > 10000 {
            raise FraudDetected { order_id: order_id, reason: "high value order" }
        }
    }
}

5. Modify the api stage to call fraud.check_order:

stage api[db: Database] {
    fn handle_order(req: OrderRequest) OrderResponse {
        let user = auth.verify_user(req.token)!
        let inventory = warehouse.check_stock(req.items)!
        let order = self.db.create_order(user.id, req.items)!
        fraud.check_order(order.id, order.total)!  // NEW
        payments.charge_async(order.id, order.total)
        return OrderResponse { order_id: order.id }
    }
}

6. Type-check — check() verifies the edit is correct
7. Commit — the SDK updates the .pluto binary with the new stage and the modified function

The compiler re-compiles. It sees that handle_order now calls fraud.check_order, which can raise FraudDetected. It:

• Adds FraudDetected to the error set of handle_order
• Generates RPC code for the api → fraud call
• Generates a new build/fraud binary
• Updates build/api to include the RPC client for fraud

You never wrote serialization code. You never wrote error handling boilerplate. The compiler generated it.

You Deploy to Production

You write a deployment spec (YAML, HCL, or future Pluto-native format):

# deploy.yaml
stages:
  api:
    replicas: 5
    region: us-east-1
    cpu: 2
    memory: 4GB

  auth:
    replicas: 2
    region: us-east-1
    cpu: 1
    memory: 2GB

  warehouse:
    replicas: 3
    region: us-west-2
    cpu: 2
    memory: 4GB

  payments:
    replicas: 2
    region: us-east-1
    cpu: 1
    memory: 2GB

  fraud:
    replicas: 1
    region: us-east-1
    cpu: 1
    memory: 1GB

You run pluto deploy --spec deploy.yaml (hypothetical command for a future orchestrator). It:

1. Builds Docker images for each stage binary
2. Pushes them to a container registry
3. Deploys them to Kubernetes (or Nomad, or EC2, or wherever)
4. Configures service discovery so stages can find each other
5. Injects config (database URLs, API keys) as environment variables

The stages start up. They discover each other via DNS or Consul. The api stage handles requests and calls auth, warehouse, fraud, and payments via HTTP. The RPC code handles serialization, retries, timeouts, error propagation — all generated by the compiler.

A Schema Change Propagates Automatically

You realize OrderRequest needs a new field: discount_code.

You edit main.pluto:

class OrderRequest {
    token: string
    items: Array<Item>
    discount_code: string?  // NEW: optional discount code
}

You re-compile. The compiler:

• Updates the serialization code for OrderRequest in the api stage
• Updates the deserialization code in any stage that receives OrderRequest (none in this case, but if warehouse needed it, the compiler would update warehouse too)
• Type-checks all usages of OrderRequest to ensure they handle the new field correctly

No manual Protobuf schema update. No “rebuild all the services that depend on this.” The compiler saw the change, propagated it, and verified it.

The Database Schema is Part of Your Program

(Aspirational — schema-as-code isn’t implemented yet.)

Eventually, your database schema will be declared in your program:

stage db {
    schema Order {
        id: string primary key
        user_id: int foreign key User(id)
        items: json
        total: int
        created_at: timestamp
    }

    pub fn create_order(user_id: int, items: Array<Item>) Order {
        return insert_into!(Order, {
            id: generate_uuid(),
            user_id: user_id,
            items: items,
            total: calculate_total(items),
            created_at: now()
        })
    }
}

The compiler generates:

• SQL migrations (CREATE TABLE, ALTER TABLE) based on schema changes
• Type-checked queries (insert_into! macro validates that all required fields are present)
• Query result types (the return type of create_order matches the Order schema)

When you change the schema (add a field, change a type, add an index), the compiler generates the migration. When you deploy, the migration runs before the stage starts. Schema changes are code changes. They’re type-checked, versioned, and deployed atomically.

Observability is Generated

(Aspirational — observability hooks aren’t implemented yet.)

The compiler knows every function call, every error, every stage boundary. It can generate observability hooks automatically:

stage api[db: Database] {
    @traced  // compiler generates tracing spans
    @metrics  // compiler generates latency/error metrics
    fn handle_order(req: OrderRequest) OrderResponse {
        let user = auth.verify_user(req.token)!
        let inventory = warehouse.check_stock(req.items)!
        let order = self.db.create_order(user.id, req.items)!
        fraud.check_order(order.id, order.total)!
        payments.charge_async(order.id, order.total)
        return OrderResponse { order_id: order.id }
    }
}

The compiler generates code that:

• Creates a trace span for handle_order
• Creates child spans for each cross-stage call (auth.verify_user, warehouse.check_stock, etc.)
• Emits metrics for latency (p50, p95, p99) and error rates
• Logs errors with structured context (order_id, user_id, error type)

You write business logic. The compiler generates the plumbing.

This is the Vision

A world where:

• You write one program with stages, not services in separate repos
• The compiler sees everything and generates RPC, serialization, migrations, metrics
• AI agents write code using the SDK, not text editors
• Deployment is configuration, not code
• Your distributed system is type-checked, error-checked, and optimized as a whole

This is not a fantasy. The pieces exist:

• Whole-program compilation ✅
• Error inference ✅
• Dependency injection ✅
• AI SDK and MCP server ✅
• Binary AST format ✅

What’s left:

• Stages and cross-stage RPC generation
• Schema-as-code and migration generation
• Observability hooks
• Orchestration integration

The foundation is solid. The vision is clear. Pluto is building toward a world where your infrastructure is your compiler, not your YAML files.

Verified Distribution

This chapter is direction, not documentation. The foundations described here — entities, typestates, compile-time invariant proofs (single- and two-state), ensures postconditions, guarded_by dominance, error-set shrinking, definite/ambiguous failure classification — are shipped and covered in Part 2. The destination they point at — a proof kernel that makes distributed-systems correctness a library concern — is not. Code blocks marked illustrative do not parse today. Everything else is shipped syntax, verified against the current compiler — including the one snippet the compiler rejects, which is the point of that snippet — and every quoted diagnostic is real output.

A brass token, 1850

On a single-track railway there is one way to die that matters more than all the others: two trains entering the same section from opposite ends. The 1850s answer was not a procedure manual and not a faster telegraph. It was a physical object — the token, a brass staff, one per section of track. A driver may not enter the section without holding it. To give it to the next train you must give it up. It cannot be duplicated, it cannot be quietly dropped in a ditch, and when a train terminates, the token goes back to the frame. Token-block signaling is where the phrase fencing token comes from: a linear, must-release capability, made of brass, a hundred and seventy years before anyone wrote down linear types.

Railway signaling invented the linear capability. Aviation invented the revocable warrant, the fence at the point of effect, and the ownership handoff. Finance invented the idempotency key and the serialized authority. The power grid invented the must-release lock with conjunctive holders. Medicine invented the identity check at the point of effect and evidence with an expiry. Five industries, each paying for the lesson in lives or money, each unaware of the others’ vocabulary — and they converged on the same small set of constructs. The constructs in this book are not novel. They have just never been compiler-checked. That is this chapter’s claim, and the rest of it is the evidence.

The bug every distributed system has

An ordinary language has an ontic semantics: program state is the world. A read gives you the truth; memory is authoritative; “what I know” and “what is” coincide. Every mainstream language is built on that identity, which is why none of them needs a concept of knowledge at all.

Distribution breaks the identity. The moment part of the world lives outside the process, every value you hold about it stops being the world and becomes a belief about the world — a snapshot, acquired at some moment, on some warrant, valid under some conditions. Regular languages cannot express the difference between “x is the balance” and “x is what the balance was when I asked.” So programmers do the epistemic bookkeeping in their heads, and every classic distributed bug is that bookkeeping failing:

• using a lease after the coordinator revoked it,
• retrying a write whose outcome was unknown,
• reporting an ambiguous outcome as a definite failure,
• trusting a cached read as current truth.

These are all the same error: acting on a warrant weaker than the action requires. Ordinary languages cannot catch this error because they cannot state it.

Pluto’s bet is that a whole-program compiler can. A program is a knower; its state is a body of claims with justifications; the compiler audits the justifications. This is the Halpern–Moses tradition — distributed protocols analyzed as transformations of knowledge states, two-generals as the impossibility of common knowledge over lossy channels — put inside a language, where it has never lived. Moses’ Knowledge of Preconditions principle says that in any correct protocol, a process taking an action that requires some fact must know that fact when acting. Correct distributed programs already satisfy this implicitly, in their authors’ heads — and, as the rest of this chapter shows, correct industries already satisfy it explicitly, in their regulations. The one-sentence version: the compiler should enforce it — refusing to compile programs whose actions outrun their knowledge.

The warrant gradient

Claims differ in how they are justified, strongest to weakest:

Two structural observations fall out:

A sound type is a claim at level 1 or 2. “I acquired and have not released” survives from check to use because only you can change it — which is exactly what a Lease<Held> typestate claims, and why it is honest. “The coordinator currently considers me the holder” is level 5 — the world can falsify it between any two instructions — and any design that encodes it statically is lying. This is why typestate never lives on a shared entity in Pluto, and why the lease example’s revocation arrives as a typed Degraded error rather than being promised away by a type.

Monotone facts are the exception that proves the ladder. A claim that once true can never be false — “the epoch is at least 42,” “the set contains x” — can be cached and shared at level-5 warrant forever, because nothing can invalidate it. This is the CALM insight (monotone means coordination-free), and it is why monotonicity was the first two-state proof shape to ship: invariant self.epoch >= old(self.epoch) is a compile-time theorem today, not a roadmap item.

No domain makes the gradient more honest than spaceflight, because there the staleness is enforced by physics. A Mars rover driver’s belief about the vehicle is fourteen light-minutes old at best — there is no “just check again.” So the discipline is total: commands are armed through a typestate chain (build, validate, arm, execute — each step gated on the one before, exactly a Command<Armed> that cannot exist without a Command<Validated>); a lost command acknowledgment is ambiguity with no fast resolution, and operations treats it as its own state, never rounded to “it failed”; and onboard fault protection is the perfect fence — the rover rejects unsafe commands at the point of effect, regardless of what ground believes, because ground’s beliefs are known to be testimony. Nobody argues with light-speed. The rest of us have the same problem with the speed of a datacenter hop; we just lie to ourselves about it.

What the shipped language already encodes

The epistemics is not a future layer bolted on top; it names what the shipped language already does. The value/entity split is the belief/fact split: a class value is a snapshot — a belief, honest about its staleness, structurally comparable, deep-copied across concurrency because beliefs are cheap to duplicate — while an object is the referent itself, never held, only asked, identity-compared because referents are not their descriptions. Invariant discharge is closed-world knowledge: “every write path preserves balance >= 0” is only knowable because the compiler sees every write path, and only sound under concurrency because values don’t alias and entities serialize their methods. Error inference is ignorance propagation: the error set of a function is the set of ways it might leave you not knowing what you hoped; mandatory handling is the rule that ignorance must be confronted, not discarded, and error-set shrinking is the converse — a proof that removes a possibility removes the obligation to handle it.

Two problems that look unrelated — “this field’s write paths all guard against negatives, so balance >= 0 is a fact” and “this store’s fencing is correct: the epoch only increases and no write lands without a validity check” — are the same proof: an invariant discharged by examining every write site. Distribution errors become tractable precisely when they are restatements of local invariants. That compression is the thesis, stated from the compiler’s side. The industries state it from the other side.

Air traffic control: the discipline, compiled

Aviation is the best-documented case of an industry independently inventing warrant discipline — procedurally, in phraseology and regulation, at the cost of decades of accidents. Every construct in Part 2 of this book has an exact counterpart in the controller’s vocabulary, and the mappings are not analogies. They are the same constructs:

• A clearance is evidence. “Cleared to descend flight level 240” is a granted, expiring, revocable warrant — not a fact about the sky. An amendment or cancellation is degradation: the world moved you out of a state you did not choose to leave.
• Readback/hearback is the fence. The pilot reads the clearance back; the controller validates it against the current picture at the point of effect. A stale clearance — superseded by an amendment the pilot hasn’t heard — is rejected there, by the authority, never by the holder’s own opinion of its validity.
• Handoff is linear ownership transfer. The rule is verbatim must-release linearity: every aircraft is under positive control of exactly one controller at all times. A track is never dropped. It is handed off or terminated — the only two exits.
• The aircraft track is an entity. It is THE plane, not a snapshot of it; sectors are domains; the flight strip is the handle one controller holds.
• Separation is the invariant — a property quantified across all tracks, which is exactly what marks it as the far horizon (more below).

Here is the track and its fence, in shipped syntax — the sketch compiles and runs today:

error StaleClearance {
    seq: int
    current: int
}

// Evidence, not authority: the clearance as issued, carried by the pilot.
class Clearance {
    seq: int
    altitude: int
}

object AircraftTrack {
    callsign: string
    altitude: int
    seq: int        // newest clearance sequence — an amendment bumps it

    invariant self.seq >= 0

    // Amending IS the invalidation: every earlier clearance is now stale.
    fn amend(mut self, altitude: int) Clearance {
        self.seq = self.seq + 1
        return Clearance { seq: self.seq, altitude: altitude }
    }

    // The readback/hearback fence: validity judged at the point of
    // effect, by the authority — never by the possibly-out-of-date holder.
    fn execute(mut self, c: Clearance) {
        if c.seq != self.seq {
            raise StaleClearance { seq: c.seq, current: self.seq }
        }
        self.altitude = c.altitude
    }
}

And the handoff, as a must-release typestate (also shipped):

class Offered { tag: int }
class UnderControl { tag: int }
class Closed { tag: int }

// The flight strip: one per aircraft, held by exactly one controller.
class Strip<S> {
    callsign: string

    must_release UnderControl

    fn accept(self) Strip<UnderControl> where S == Offered {
        return Strip<UnderControl> { callsign: self.callsign }
    }

    fn handoff(self) Strip<Offered> where S == UnderControl {
        return Strip<Offered> { callsign: self.callsign }
    }

    fn terminate(self) Strip<Closed> where S == UnderControl {
        return Strip<Closed> { callsign: self.callsign }
    }
}

Accept a strip and end your shift without discharging it — let mine = s.accept() and then just a return — and the compiler answers in the controller’s own terms (real output): 'mine' still holds Strip<UnderControl>, a must_release state, when it goes out of scope; transition it out of 'UnderControl' (e.g. .handoff()), move it onward, or return it. Positive control of exactly one controller at all times — as a type error.

Lost communication is the Definite/Ambiguous split. A pilot who stops hearing the controller does not know whether the last transmission arrived; the controller does not know what the pilot will do. No local information can resolve it — and aviation’s lost-comm procedures are the legitimate exits from ambiguity, written as regulation: fly the last acknowledged clearance (act only on fenced evidence, never on testimony that was still in flight); squawk 7600 (escalate honestly — broadcast your ignorance instead of laundering it into a guess); then follow the published procedure (resolution by protocol, agreed before the failure, because agreement during the failure is exactly what you no longer have).

The composition test: a handoff during an amendment with a comm failure

North stars are cheap when each feature gets its own slide. The real test is one scenario that needs all of them at once — and ATC runs it daily.

Sector A is handing UAL232 to sector B. Mid-handoff, A amends the descent clearance. The amendment’s acknowledgment never arrives.

Walk the constructs through it. The track is an entity: identity survives the handoff — B receives THE aircraft, not a copy whose state forked at the boundary. The clearance is a typestated value — give the Clearance sketch the Strip treatment and proposed, issued, acknowledged become different types, with “acknowledged” the only one anyone may act on. The handoff is a linear transfer: A’s strip binding is consumed, B’s is created, and no interleaving of the amendment can produce zero controllers or two. The amendment is degradation: the old clearance’s seq is dead, and the pilot’s copy of it is now provably stale evidence. The readback fence catches exactly that: if the stale clearance is executed against the track, the authority rejects it at the point of effect. The comm failure is ambiguity: the amendment may or may not have been heard, and the system’s answer is not a guess — it is the lost-comm protocol, keyed on what was acknowledged, which the typestate recorded. And separation is the invariant that must hold across every interleaving of all of the above.

Now remove any one construct and watch the scenario break — not degrade, break:

• No entity identity → A and B hold diverging snapshots of “the same” aircraft; the amendment lands on one of them.
• No typestates → nothing distinguishes an issued clearance from an acknowledged one, and the lost-comm procedure has no fact to key on.
• No linearity → a strip can be dropped mid-handoff; some aircraft is under positive control of nobody.
• No fence → the pilot’s stale clearance executes, because the holder judged its own evidence.
• No degradation channel → the amendment is a silent overwrite; the old clearance fails as a mystery instead of carrying its post-failure state.
• No Definite/Ambiguous split → the unacknowledged amendment gets rounded to “it applied” or “it didn’t,” each wrong half the time.
• No invariant → all of the above succeed locally and the aircraft converge anyway.

The features do not add; they multiply. Each one is the reason another one’s guarantee survives contact with the scenario. That is what “more than themselves” means, and aviation needed decades of accident reports to assemble the same set procedurally. This language is that discipline, compiled.

One construct in the list is beyond the shipped proof engine, and it is the one that marks the horizon. Separation is a cross-entity invariant — quantified over all tracks, not a field predicate on one:

// ILLUSTRATIVE — not shipped. Cross-entity invariants are the
// phase-4+ horizon, not the current fragment.
system Sector {
    invariant forall a, b in AircraftTrack where a != b:
        separated(a, b)
}

Today’s fragment proves single-entity facts at every write site. The roadmap’s proof shapes (below) are the steps from here to there.

The ledger: money is neither created nor destroyed

The grand claim, stated plainly: a Pluto ledger should carry conservation of money as a named, compiler-checked theorem — across all accounts, the sum of balances equals issuance minus redemption, and no interleaving of transfers, retries, or crashes can violate it. Like separation, conservation is a cross-entity invariant: honestly phase-4+, not a feature you can use today.

Unlike the rest of this chapter’s horizon, though, the ledger’s foundations are not a sketch. They compile now, and the receipts are real.

Receipt one: balance >= 0 is a proven invariant, strictly. Write the unguarded version —

class Account {
    balance: int

    invariant self.balance >= 0

    fn withdraw(mut self, amount: int) {
        self.balance = self.balance - amount
    }
}

— and the compiler rejects it at the write site, with the symbolic state it reached (real output, today):

error: cannot prove invariant 'self.balance >= 0' of class 'Account' holds
at the end of this method in method 'withdraw': at this point self.balance =
-amount + old(self.balance). The invariant may be broken temporarily between
writes, but must be re-established at every boundary (method exits, raises,
calls, loops, branch joins). Establish the missing bound before this point
with a guard, a 'requires' clause, or an 'assert'
(e.g. 'if amt <= self.balance { ... }')

No runtime check was declined here — there was never going to be one. An invariant the compiler cannot discharge is a compile error, full stop.

Receipt two: proofs delete error handling. Give Account a raising variant —

error Insufficient {
    needed: int
}

// added to Account:
fn try_withdraw(mut self, amount: int) int
    requires amount > 0
{
    if amount > self.balance {
        raise Insufficient { needed: amount }
    }
    self.balance = self.balance - amount
    return self.balance
}

— and guard the call, and the Insufficient error provably vanishes at that site. This compiles today, with no ! and no catch:

fn main() {
    let mut account = Account { balance: 100 }
    let amount = 80
    if amount <= account.balance {
        let after = account.try_withdraw(amount)   // no handler — proven safe
        print(after)
    }
}

Remove the guard and it is the usual compile error. The guard is not defensive programming; it is the proof, and the compiler read it. (examples/contracts in the repository is the runnable version.)

Receipt three: the movement itself is a theorem. With the proof-form ensures shipped, the withdrawal can state exactly what it did to the balance, and the compiler proves it at every normal exit:

fn try_withdraw(mut self, amount: int) int
    requires amount > 0
    ensures self.balance == old(self.balance) - amount
{
    if amount > self.balance {
        raise Insufficient { needed: amount }
    }
    self.balance = self.balance - amount
    return self.balance
}

This compiles today, and callers assume the relation: after a proven try_withdraw(amount), the caller’s facts carry balance == old(balance) - amount, feeding construction proofs and error-set shrinking downstream. A debit that debits exactly what it says is no longer a comment — it is the per-method half of conservation, checked. (Receipt three’s sibling shipped too: invariant self.epoch >= old(self.epoch) makes monotone fields a one-line theorem — see the blob store below.)

The rest of the ledger is the shipped vocabulary applied straight: accounts are entities — one referent per account, methods serialized, so a transfer’s debit-credit pair cannot interleave with another transfer mid-method; transfers carry idempotency keys on the wire and wear their protocol as a typestate:

class Pending { tag: int }
class Committed { tag: int }

class Transfer<S> {
    key: string      // idempotency key — rides the wire with the transfer
    amount: int

    fn commit(self) Transfer<Committed> where S == Pending {
        return Transfer<Committed> { key: self.key, amount: self.amount }
    }
}

A commit whose acknowledgment is lost is an ambiguous failure, and the key is what makes “retry” one of the legitimate exits: the retry’s outcome is knowledge. Every trader, every payments engineer already runs this protocol by hand. The theorem on the horizon is the compiler running it instead:

// ILLUSTRATIVE — not shipped. Conservation as a checked artifact.
system Ledger {
    invariant sum(Account.balance) == self.issued - self.redeemed
}

“The compiler proves money is neither created nor destroyed” is a sentence worth being honest about, so: the per-account halves of it are proven today (receipt one); the cross-entity sum is the same kind of claim as separation, and it arrives the same way.

The first fully-built protocol

The acceptance test for this direction has been built: examples/blob is a lockless, single-writer, fenced-atomic blob store — written in Pluto, running today on shipped features only. An authority entity owns the data and a fencing epoch; minting a grant advances the epoch, silently invalidating all older grants; a write presents its grant and the authority judges it at the point of effect. If the shape sounds familiar, it should: BlobAuthority.apply and AircraftTrack.execute are the same method — the fence is one construct, whether what it guards is bytes or altitudes. A loser of the race gets a definite, typed, inspectable StaleGrant — not a silent no-op and not corruption. Each guarantee has exactly one owner:

Note where safety lives: not in the client checking “is my grant still valid?” — a process can pause between the check and the write landing, and no client-side check closes that gap. The provable theorem is not “no write is attempted without a valid grant” (physics forbids proving that) but the one that matters: no write is applied without a currently-valid grant. Fencing is constructive knowledge — level 3 on the gradient. You don’t learn whether the stale write was attempted; you act so that it cannot land, which is why fencing is robust to message loss while “asking again” never is.

When this chapter was first written, that column had a hole: the store’s single-state invariants (epoch >= 0, applied <= epoch) were proven at compile time, but monotonicity (“every write to epoch increases it” — a two-state claim) and dominance (“no write to data escapes the fence” — a control-flow claim about write sites) held by inspection, not by proof. Those were the two proof shapes on the roadmap. Both have shipped, and examples/blob now carries them as clauses — this is shipped syntax, not an illustration:

object BlobAuthority {
    data: bytes guarded_by (g: WriteGrant) g.token == self.epoch
    epoch: int

    invariant self.epoch >= old(self.epoch)   // proven: no write decreases it

    fn apply(mut self, grant: WriteGrant, d: string) {
        if grant.token != self.epoch {
            raise StaleGrant { token: grant.token, epoch: self.epoch }
        }
        self.data = d.to_bytes()              // proven: dominated by the fence
    }
}

The two-state invariant is monotonicity with no keyword: every method exit and every write site must prove the epoch did not decrease, so a minted token can never become current again. The guarded_by clause makes the fence structural: every write to data, across the whole program’s closed write-set, must be dominated by a conditional the prover can show implies g.token == self.epoch — remove the fence, move the write above it, or slip a call between them, and the store stops compiling. (Both shapes are documented in Contracts; the full runnable protocol is examples/blob.)

So the safety theorem — no write is applied without a currently-valid grant — is now a checked artifact, not an inspection note. What remains is the naming layer: a property form that binds theorems like these to names (monotonic, fenced, idempotent) a library can export and downstream code can require without reading the internals — making “a lockless distributed file with provably single-writer writes” an import, not a language feature. The shipped shapes are also the on-ramp to the cross-entity horizon: separation and conservation decompose into exactly these per-entity pieces plus a quantified sum.

Properties are someone’s responsibility

The kernel deliberately stops at domain-neutral proof shapes: write-path preservation, dominance, monotone writes, linear consumption. The language will hardcode no specific distributed property — no built-in idempotent, no blessed transactional. Baking in instances of a pattern instead of the kernel that expresses them is the mistake Pluto has already rejected twice (wire-traits, typestated objects).

Instead, named properties are planned as library definitions whose meaning bottoms out in kernel shapes — and every claim of a property has a named owner and exactly one warrant:

• Proven — the kernel discharged it from the body (the dedup check provably dominates the effect).
• Checked — a runtime residual enforces it, violations raising typed errors.
• Assumed — declared explicitly at a trust boundary, visible and attributed. The ATC system’s radar feed is extern: “this track position is current” is an assume, not a proof, and it says so. A clearance relayed through an outside system carries the same honesty marker. S3’s write semantics carry assume idempotent(key).

So “retry from ambiguity” is not a language rule about idempotency. A retry combinator requires idempotent(key) of its callee; the ledger’s transfer authority provides it — by proof if the dedup table is in the compilation unit, by assumption if the processor is extern; the compiler matches requirement to provision and never loses track of who vouched. And the assumption surface becomes an artifact: pluto analyze reporting every claim discharged by assumption rather than proof — the complete list of things your deployment rests on that nobody proved. A deployment’s honesty, as a report.

Failure classification gets the same treatment — and this piece has shipped. Every failure of an effectful boundary call is one of exactly two kinds — definite (the effect is known not to have applied: connection refused before send, the authority’s fence rejected it) or ambiguous (the request left; nothing came back; no local information can say). Ambiguity has exactly four legitimate exits: idempotent retry, read-back, self-fencing, or honest escalation — the same four aviation wrote into its lost-comm regulations. The runtime owns the classification — only it knows whether bytes left the socket — and today it delivers it on every boundary failure as NetworkError.definite, set truthfully: definite only with a warrant, ambiguous whenever in doubt. What stays library policy with property requirements is everything built on top — the retry combinator that demands idempotency before consuming an ambiguous failure, the read-back, the escalation.

Why this and not a framework

Every piece of this exists somewhere: epistemic logic has modeled distributed protocols since the 1980s; session types track protocol position; CRDT languages own the monotone corner; TLA+ can model all of it — outside the program, unchecked against the code you actually ship. The gap Pluto occupies is the combination: a type system that audits how you know, checked by a whole-program compiler that sees both sides of every boundary.

No modal logic will surface in user syntax — no knowledge operators, no belief algebra. The constructs you have already seen are the surface syntax of warrants: typestates for what you did, invariants for what every path preserves, entities for referents, values for beliefs, typed errors for ignorance, at for questions asked across a boundary. The epistemics is the design lens that keeps those constructs honest, and the verification engine is the machinery that turns the lens into rejected programs.

The concept chapters trace the same pattern library through the rest of reality: the exchange whose single-threaded matching engine is entity serialization at world scale (Objects, Concurrency); the web’s famously broken certificate revocation, which is a belief outliving its warrant (Contracts); the electrician’s lockout-tagout padlock, which is a must-release token you hold in your hand (Typestates); the transfusion ward’s wristband check, which is the fence at the point of effect (Objects). Even organ allocation runs the protocol: an organ is offered to exactly one center at a time, under a hard deadline, with the cold-ischemia clock as the revoking authority — a linear, expiring warrant, administered by fax and phone call.

None of these industries waited for language support. They built warrants, fences, and linear evidence out of brass, phraseology, padlocks, and wristbands, because the alternative was collisions, mid-airs, double-spends, electrocutions, and wrong-blood transfusions. The language will not ship distributed-systems constructs, and it will not ship aviation constructs either. It will ship a proof kernel — and the difficult machinery (leases, fencing, epochs, handoffs, single-writer stores, idempotent handlers) becomes libraries whose correctness theorems the compiler checks, the same way it checks yours.

std.base64

Base64 encoding and decoding.

import std.base64

Functions

encode

base64.encode(s: string) string

Encodes a string to standard base64.

let encoded = base64.encode("hello world")
// "aGVsbG8gd29ybGQ="

decode

base64.decode(s: string) string

Decodes a standard base64 string.

let decoded = base64.decode("aGVsbG8gd29ybGQ=")
// "hello world"

encode_bytes / decode_bytes

base64.encode_bytes(b: bytes) string
base64.decode_bytes(s: string) bytes

Standard base64 over a bytes buffer, exact for every byte value (the string forms are for text).

let enc = base64.encode_bytes("hi".to_bytes())    // "aGk="
let raw = base64.decode_bytes(enc)                // 2 bytes

encode_url_safe

base64.encode_url_safe(s: string) string

Encodes a string to URL-safe base64 (uses - and _ instead of + and /).

decode_url_safe

base64.decode_url_safe(s: string) string

Decodes a URL-safe base64 string.

Example

import std.base64

fn main() {
    let original = "hello world"
    let encoded = base64.encode(original)
    let decoded = base64.decode(encoded)
    print(f"Encoded: {encoded}")
    print(f"Decoded: {decoded}")
}

std.collections

Functional operations on arrays. All higher-order functions take closures as arguments.

import std.collections

Types

Pair<A, B>

A generic two-element tuple used by zip and enumerate.

pub class Pair<A, B> {
    first: A
    second: B
}

Transforms

map

collections.map<T, U>(arr: [T], f: fn(T) U) [U]

Applies f to each element, returns a new array of results.

let doubled = collections.map([1, 2, 3], (x: int) => x * 2)
// [2, 4, 6]

flat_map

collections.flat_map<T, U>(arr: [T], f: fn(T) [U]) [U]

Maps each element to an array, then flattens the result.

let expanded = collections.flat_map([1, 2, 3], (x: int) => [x, x * 10])
// [1, 10, 2, 20, 3, 30]

filter

collections.filter<T>(arr: [T], f: fn(T) bool) [T]

Returns elements for which f returns true.

let evens = collections.filter([1, 2, 3, 4], (x: int) => x % 2 == 0)
// [2, 4]

Reductions

fold

collections.fold<T, U>(arr: [T], initial: U, f: fn(U, T) U) U

Left fold with an initial accumulator value.

let sum = collections.fold([1, 2, 3], 0, (acc: int, x: int) => acc + x)
// 6

reduce

collections.reduce<T>(arr: [T], f: fn(T, T) T) T

Like fold, but uses the first element as the initial value. Array must be non-empty.

let product = collections.reduce([2, 3, 4], (a: int, b: int) => a * b)
// 24

sum / sum_float

collections.sum(arr: [int]) int
collections.sum_float(arr: [float]) float

collections.sum([10, 20, 30])          // 60
collections.sum_float([1.5, 2.5])      // 4.0

Predicates

any / all

collections.any<T>(arr: [T], f: fn(T) bool) bool
collections.all<T>(arr: [T], f: fn(T) bool) bool

collections.any([1, 2, 3], (x: int) => x > 2)    // true
collections.all([1, 2, 3], (x: int) => x > 0)     // true

count

collections.count<T>(arr: [T], f: fn(T) bool) int

Returns the number of elements satisfying f.

collections.count([1, 2, 3, 4, 5], (x: int) => x > 3)    // 2

Slicing and Reordering

reverse / take / drop

collections.reverse<T>(arr: [T]) [T]
collections.take<T>(arr: [T], n: int) [T]
collections.drop<T>(arr: [T], n: int) [T]

collections.reverse([1, 2, 3])     // [3, 2, 1]
collections.take([1, 2, 3, 4], 2)  // [1, 2]
collections.drop([1, 2, 3, 4], 2)  // [3, 4]

flatten

collections.flatten<T>(arr: [[T]]) [T]

Flattens one level of nesting.

collections.flatten([[1, 2], [3], [4, 5]])    // [1, 2, 3, 4, 5]

Combining

zip

collections.zip<A, B>(a: [A], b: [B]) [Pair<A, B>]

Pairs elements by index. Result length equals the shorter array.

let names = ["alice", "bob"]
let scores = [95, 87]
let pairs = collections.zip(names, scores)
// pairs[0].first == "alice", pairs[0].second == 95

enumerate

collections.enumerate<T>(arr: [T]) [Pair<int, T>]

Pairs each element with its index.

let indexed = collections.enumerate(["a", "b", "c"])
// Pair { first: 0, second: "a" }, Pair { first: 1, second: "b" }, ...

Side Effects

for_each

collections.for_each<T>(arr: [T], f: fn(T))

Calls f on each element. Returns void.

collections.for_each(["alice", "bob"], (name: string) => {
    print(f"hello {name}")
})

Sorting

All sorts return a new array and leave the input untouched. They are stable (equal elements keep their order) and run in O(n log n).

sort_by

collections.sort_by<T>(arr: [T], less: fn(T, T) bool) [T]

Sorts with less(a, b), which returns true when a should come strictly before b.

let desc = collections.sort_by([1, 3, 2], (a: int, b: int) => a > b)    // [3, 2, 1]

sort / sort_floats / sort_strings

collections.sort(arr: [int]) [int]
collections.sort_floats(arr: [float]) [float]
collections.sort_strings(arr: [string]) [string]

Ascending order. Strings sort byte-wise, as strings.compare does.

collections.sort([3, 1, 2])                          // [1, 2, 3]
collections.sort_strings(["pear", "apple", "fig"])   // ["apple", "fig", "pear"]

Fallible Callbacks

collections.try_map<T, U>(arr: [T], f: fn(T) U!) [U]
collections.try_filter<T>(arr: [T], f: fn(T) bool!) [T]
collections.try_fold<T, U>(arr: [T], initial: U, f: fn(U, T) U!) U
collections.try_for_each<T>(arr: [T], f: fn(T)!)

Variants of map, filter, fold and for_each whose callback may raise. The first error stops the walk and propagates to the caller, so a call must be handled with ! or catch. Infallible callbacks are accepted too.

let halves = collections.try_map([4, 8], halve)!    // [2, 4]
let safe = collections.try_map(inputs, halve) catch err {
    let none_left: [int] = []
    none_left
}

Example: Pipeline

import std.collections

fn main() {
    let data = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10]
    let even_data = collections.filter(data, (x: int) => x % 2 == 0)
    let squared = collections.map(even_data, (x: int) => x * x)
    let total = collections.fold(squared, 0, (acc: int, x: int) => acc + x)
    print(f"sum of even squares: {total}")
    // sum of even squares: 220
}

std.env

Environment variable access.

import std.env

Functions

get

env.get(name: string) string

Returns the value of the environment variable, or an empty string if not set.

get_or

env.get_or(name: string, default_val: string) string

Returns the value of the environment variable, or default_val if not set.

let port = env.get_or("PORT", "8080")

set

env.set(name: string, value: string)

Sets an environment variable.

exists

env.exists(name: string) bool

Returns true if the environment variable is set.

list_names

env.list_names() [string]

Returns an array of all environment variable names.

remove

env.remove(name: string) bool

Removes an environment variable. Returns true if it existed.

Example

import std.env

fn main() {
    let host = env.get_or("DATABASE_HOST", "localhost")
    let port = env.get_or("DATABASE_PORT", "5432")
    print(f"Connecting to {host}:{port}")
}

std.fs

File system operations: one-shot helpers for the common cases, an atomic durable replace, and a typestated file handle whose protocol — open, use, close — is checked by the compiler.

import std.fs

The design premise: the OS is the authority over the real file state, and a File value is evidence — a capability the authority minted at open, which you must eventually hand back. Leaking a handle, using it after close, writing through a read handle, or retrying a failed sync are not runtime errors in this module; they are programs that do not compile. See Typestates for the machinery.

Errors

pub error NotFound { path: string }                                 // ENOENT
pub error FileError { path: string, code: int, message: string }    // any other OS failure
pub error CloseError { code: int, message: string }                 // close() failed; fd released regardless
pub error SyncError { path: string, code: int, message: string }    // one-shot durability failure
pub error Degraded { file: File<Write, Poisoned>, code: int, message: string }

The split is by what callers do, not by errno taxonomy. NotFound is the one branch-worthy case (the 404 shape, config defaulting) and gets its own type; everything else definite is a FileError carrying the path and the raw errno captured at the syscall site — no string matching. CloseError, SyncError, and Degraded are distinct so a generic handler cannot accidentally absorb a durability loss; Degraded is covered under File Handles below.

(FileError.path is "" when raised by a handle method like read or seek — the handle carries only a descriptor, not the path it was opened from.)

Quick Read/Write

read_all / write_all / append_all

fs.read_all(path: string) string           // raises NotFound | FileError
fs.write_all(path: string, data: string)   // raises NotFound | FileError
fs.append_all(path: string, data: string)  // raises NotFound | FileError

fs.write_all("hello.txt", "hello, world")!
let content = fs.read_all("hello.txt")!
fs.append_all("hello.txt", "\nmore data")!

Binary-safe variants take and return bytes instead of a string:

fs.read_all_bytes(path: string) bytes           // raises NotFound | FileError
fs.write_all_bytes(path: string, data: bytes)   // raises NotFound | FileError
fs.append_all_bytes(path: string, data: bytes)  // raises NotFound | FileError

The descriptor lives and dies inside the call, so no handle value appears — and close errors are folded into the result: success means the bytes were written and the descriptor closed cleanly. (On NFS-class filesystems, close is where deferred write errors surface; these helpers do not swallow them.)

Durable Replace

replace_all

fs.replace_all(path: string, data: string)   // raises NotFound | FileError | SyncError

The atomic durable update, packaged: write a temp file in the same directory, sync it to full durability, rename it over path, then fsync the parent directory (the name→inode mapping is the directory’s dirty page, not the file’s). Readers see either the old contents or the new contents, never a torn mix, and a crash after success cannot roll the update back.

The error contract is two-sided — the type tells you what survived:

• FileError (or NotFound) ⇒ the old file is intact. The failure happened before the rename; the temp file was cleaned up.
• SyncError ⇒ the rename landed, but its durability is unwarranted — the directory fsync failed, so a crash could still lose it.

fs.replace_all(config, "retries = 5\n") catch e: fs.SyncError {
    // New config IS in place, durability unwarranted. Treat as failed; alert.
    print(f"replace landed without durability warrant: {e.message}")
    return
} catch e: fs.FileError {
    // Old config intact; temp cleaned up. Safe to retry or report.
    print(f"replace failed, old config intact: {e.message}")
    return
}

The four steps are packaged because this is the only safe traversal, and intermediate failures must clean up the temp file.

replace_all_bytes

fs.replace_all_bytes(path: string, data: bytes)   // raises NotFound | FileError | SyncError

The bytes variant of replace_all, for binary files (logs, snapshots, indexes): the same temp → sync → rename → sync-dir sequence and the same error contract.

sync_dir

fs.sync_dir(path: string)   // raises SyncError

fsync a directory — required for crash-safe rename/create/remove compositions you build yourself. One-shot by nature; there is no directory handle.

File Handles

For streaming or partial reads and writes, open a handle:

fs.open_read(path: string) File<Read, Open>      // raises NotFound | FileError
fs.open_write(path: string) File<Write, Open>    // O_WRONLY|O_CREAT|O_TRUNC
fs.open_append(path: string) File<Write, Open>   // O_WRONLY|O_CREAT|O_APPEND

File<M, S> is a typestated class — a value carrying evidence, not an entity. The mode M (Read or Write) is fixed at open; the state S (Open, Poisoned, or Closed) changes only through consuming transitions. Append-ness lives in the descriptor (O_APPEND), not the type, so open_append also yields a File<Write, Open>.

Three guarantees ride on the type:

• Leaks are compile errors. Open and Poisoned are must_release states: dropping a live handle, capturing it in a closure or spawn, or storing it in a field is rejected at compile time, with a diagnostic naming the obligation and the transitions out.
• Method existence is per-state. read exists only where M == Read, S == Open; write, sync, and sync_data only where M == Write, S == Open. Use-after-close, double-close, and write-on-a-read-handle are not runtime errors — the methods do not exist on those types.
• Transitions consume. close() consumes the binding and returns a File<M, Closed>, which is inert and droppable — so f.close()! in statement position fully discharges the obligation. Using the old binding afterwards is a compile error.

Methods on File<M, Open>

file.read(max_bytes: int) string     // M == Read; "" means EOF; raises FileError
file.write(data: string)             // M == Write; writes ALL of data; raises Degraded
file.sync()                          // M == Write; full durability; raises Degraded
file.sync_data()                     // M == Write; data + size only; raises Degraded
file.seek(to: Seek) int              // either mode; returns new offset; raises FileError
file.close() File<M, Closed>         // consuming transition; raises CloseError

read requires max_bytes > 0 (a compile-time contract — see Contracts) and returns "" only at EOF; a failure raises, so an empty string is never a disguised error. write loops to completion: success means every byte reached the OS, short writes are never silently dropped.

seek takes a Seek target instead of whence magic ints, constructed with dotted enum syntax:

pub enum Seek {
    Start { offset: int }
    Current { delta: int }
    End { delta: int }
}

let f = fs.open_read(path)!
let first5 = f.read(5)!
f.seek(fs.Seek.Start { offset: 0 })!
let all = f.read(1024)!
f.close()!

close() surfaces its result as CloseError — but either way the descriptor is gone (POSIX deallocates it even when close fails), so the error is a durability report, not a retry invitation.

Durability: sync and sync_data

sync() means full durability on every platform: after it returns, everything previously written through this descriptor is on stable storage — fsync on Linux, fcntl(F_FULLFSYNC) on Darwin, because Darwin’s plain fsync does not flush the drive’s volatile cache. Strong is the default; if F_FULLFSYNC is unsupported (SMB/NFS mounts), the call raises rather than silently degrading. sync_data() skips metadata-only flushes (fdatasync on Linux; on Darwin there is no honest cheaper form, so it is F_FULLFSYNC too).

One honest caveat: the implementation is syscall-faithful, not crash-tested — CI verifies the right syscalls are issued and the error paths are honest; actual power-loss durability depends on the drive’s firmware telling the truth.

Degradation: a failed write or sync poisons the handle

A failed write or sync destroys the durability warrant for the descriptor: after a failed write the prefix state is unknown, and after a failed sync the kernel has reported the writeback error once and marked the pages clean — it cannot re-issue the report, so a retried sync would succeed while your data is gone. (This is the “fsyncgate” failure mode that silently corrupted PostgreSQL data for years.)

std.fs encodes the rule in the type system. The failure raises Degraded, whose payload carries the handle in its honest post-failure state:

pub error Degraded { file: File<Write, Poisoned>, code: int, message: string }

Catching Degraded consumes the Open binding — the value now lives in e.file as a File<Write, Poisoned>. The only method on a poisoned handle is the discharge:

file.discard() File<M, Closed>   // the only exit from Poisoned; never raises

Calling sync or write on a poisoned handle is a type error: the method to retry does not exist on the type the failure hands you. And because the payload is itself must_release, a wildcard catch cannot swallow a Degraded — only a typed handler, which takes on the obligation, is legal. Recovery is reopening and rewriting from data the program still owns, or crashing and recovering from a log.

The write-ahead-log shape, from examples/durable_config:

error ConfigDead { reason: string }

fn append_durably(w: fs.File<fs.Write, fs.Open>, entry: string) fs.File<fs.Write, fs.Open> {
    w.write(entry) catch e: fs.Degraded {
        let p = e.file
        p.discard()
        raise ConfigDead { reason: f"write failed (errno {e.code})" }
    }
    w.sync_data() catch e: fs.Degraded {
        let p = e.file
        p.discard()
        raise ConfigDead { reason: f"sync failed (errno {e.code}); reopen and rewrite" }
    }
    return w
}

The obligation travels: in through the parameter, back through the return, and on failure into the error payload, where the handler discards it and reports upstream. The caller holds the handle in a local across batches:

let mut wal = fs.open_append(dir + "/changes.log")!
wal = append_durably(wal, "set retries 5\n")!
wal = append_durably(wal, "set timeout_ms 200\n")!
wal.close()!

Forgetting wal.close() is not a bug to find in review — it is a compile error naming the obligation.

Metadata

stat

fs.stat(path: string) Metadata   // raises NotFound | FileError

pub class Metadata {
    size: int        // bytes; invariant: size >= 0
    modified: int    // unix seconds
    is_dir: bool
    is_file: bool
    mode: int        // permission bits
}

Metadata carries a compile-time invariant size >= 0, proven at its construction site inside std.fs — callers get to assume it for free.

Path queries

fs.exists(path: string) bool
fs.is_file(path: string) bool
fs.is_dir(path: string) bool
fs.file_size(path: string) int     // = stat(path).size; raises NotFound | FileError

File Operations

fs.remove(path: string)                   // delete a file; raises NotFound | FileError
fs.rename(from: string, to: string)       // rename or move; raises NotFound | FileError
fs.copy(from: string, to: string)         // copy; close errors surfaced; raises NotFound | FileError
fs.truncate(path: string, len: int)       // set the file's length; raises NotFound | FileError

truncate matches write_all’s durability stance: success means the kernel accepted the new length, not that it is durable. To make a shrink durable, use the handle form (open_append → truncate → sync → close).

Directory Operations

fs.mkdir(path: string)                    // create one directory; raises NotFound | FileError
fs.create_dir_all(path: string)           // mkdir -p; existing directory is success
fs.rmdir(path: string)                    // remove empty directory; raises NotFound | FileError
fs.remove_dir_all(path: string)           // recursive delete; refuses "/" and ""
fs.list_dir(path: string) [string]        // list entries; raises NotFound | FileError
fs.temp_dir() string                      // system temp directory

remove_dir_all unlinks symlinks rather than following them.

Example: Durable Config Update

import std.fs

fn main() {
    let dir = fs.temp_dir()
    let config = dir + "/app.conf"

    fs.write_all(config, "retries = 3\n")!
    print(f"before: {fs.read_all(config)!}")

    fs.replace_all(config, "retries = 5\ntimeout_ms = 200\n") catch e: fs.SyncError {
        print(f"replace landed without durability warrant: {e.message}")
        return
    } catch e: fs.FileError {
        print(f"replace failed, old config intact: {e.message}")
        return
    } catch e: fs.NotFound {
        print(f"missing: {e.path}")
        return
    }
    print(f"after:  {fs.read_all(config)!}")

    fs.remove_dir_all(dir)!
}

The full version — including the WAL half with open_append, per-batch sync_data, and honest degradation — is examples/durable_config/main.pt; the plain file I/O tour is examples/file_io/main.pt.

std.http

HTTP/1.1 server with request parsing and response helpers.

import std.http

Errors

pub error HttpError {
    message: string
}

Raised by listen() and HttpConnection.read_request().

Entities and Invariants

HttpServer and HttpConnection are objects — entities owning live sockets. They compare by identity, are shared (not deep-copied) across spawn, and their methods serialize per instance. Request and Response stay classes: they are wire-shaped data, copied and compared structurally. See Objects and Entities.

Both entities carry a compile-time-proven invariant: self.fd >= 0. A HttpServer or HttpConnection can never exist around a bad descriptor — listen() raises HttpError on any socket/bind/listen failure instead of constructing a broken server, and accept() raises instead of wrapping a failed descriptor. The invariant is discharged statically (see Contracts); no runtime check exists.

Server

listen

http.listen(host: string, port: int) HttpServer    // raises HttpError

Binds an HTTP server socket.

HttpServer

HttpConnection

Request

pub class Request {
    method: string        // "GET", "POST", etc.
    path: string          // "/hello", "/users/123"
    headers_raw: string   // raw header block
    body: string          // request body
}

Response Helpers

Convenience constructors for common responses:

http.ok(body: string) Response                                      // 200, text/plain
http.ok_json(json_string: string) Response                          // 200, application/json
http.not_found() Response                                           // 404
http.bad_request() Response                                         // 400
http.response(status: int, status_text: string, body: string) Response   // custom status

Response

pub class Response {
    status: int
    status_text: string
    headers_raw: string
    body: string
}

Example: JSON API

import std.http
import std.json

fn handle(req: http.Request) http.Response {
    if req.path == "/hello" {
        let mut body = json.object()
        body.set("message", json.string("Hello, World!"))
        return http.ok_json(body.to_string())
    }

    if req.path == "/echo" {
        if req.method == "POST" {
            let data = json.parse(req.body) catch json.Json {
                tag: 0, int_val: 0, float_val: 0.0,
                string_val: "", children: [], keys: []
            }
            let mut resp = json.object()
            resp.set("echo", data)
            return http.ok_json(resp.to_string())
        }
        return http.bad_request()
    }

    return http.not_found()
}

fn main() {
    let server = http.listen("0.0.0.0", 8080)!
    print("Listening on :8080")

    while true {
        let conn = server.accept()!
        let req = conn.read_request() catch http.Request {
            method: "", path: "", headers_raw: "", body: ""
        }
        if req.method != "" {
            conn.send_response(handle(req))
        }
        conn.close()
    }
}

std.io

Console I/O: printing without newlines and reading from stdin.

import std.io

Functions

print / println

io.print(s: string)      // write to stdout, no trailing newline
io.println(s: string)    // write to stdout with trailing newline

Note: The built-in print() (no import needed) already prints with a newline. io.print() is useful when you need to write a prompt on the same line as user input.

read_line

io.read_line() string

Reads one line from stdin (blocking). Returns the input without the trailing newline.

Example: Interactive Prompt

import std.io

fn main() int? {
    io.print("What is your name? ")
    let name = io.read_line()
    print(f"Hello, {name}!")

    io.print("Enter a number: ")
    let n = io.read_line().to_int()?
    print(f"Doubled: {n * 2}")

    return none
}

to_int() returns int? – it yields none if the string is not a valid integer. The ? operator propagates the none value, causing the function to return early.

std.json

Parse, build, and stringify JSON. The module provides a single Json value type that represents all JSON forms.

import std.json

Errors

pub error JsonError {
    message: string
}

json.parse() raises JsonError on invalid input.

Constructors

Build JSON values programmatically:

json.null() Json
json.bool(v: bool) Json
json.int(v: int) Json
json.float(v: float) Json
json.string(v: string) Json
json.array() Json
json.object() Json

let obj = json.object()
obj.set("name", json.string("Alice"))
obj.set("age", json.int(30))
obj.set("active", json.bool(true))

let items = json.array()
items.push(json.int(1))
items.push(json.int(2))
obj.set("scores", items)

Parsing

json.parse(s: string) Json     // raises JsonError

let data = json.parse("{\"name\": \"Alice\", \"age\": 30}")!
let name = data.get("name").get_string()
let age = data.get("age").get_int()

Json Methods

Type Checks

j.is_null() bool
j.is_bool() bool
j.is_int() bool
j.is_float() bool
j.is_string() bool
j.is_array() bool
j.is_object() bool

Value Extraction

j.get_bool() bool
j.get_int() int
j.get_float() float
j.get_string() string

get_int() on a float value truncates. get_float() on an int value converts.

Traversal

j.get(key: string) Json     // object field lookup; returns json.null() if missing
j.at(index: int) Json       // array index access
j.len() int                 // array or object length

Mutation

j.set(key: string, value: Json)    // set or overwrite an object field
j.push(value: Json)                // append to an array

Serialization

j.to_string() string    // JSON-encoded string

Example: Round-Trip

import std.json

fn main() {
    let mut response = json.object()
    response.set("status", json.string("ok"))
    response.set("count", json.int(3))

    let mut items = json.array()
    items.push(json.string("apple"))
    items.push(json.string("banana"))
    response.set("items", items)

    let s = response.to_string()
    print(s)
    // {"status":"ok","count":3,"items":["apple","banana"]}

    let parsed = json.parse(s)!
    print(parsed.get("status").get_string())    // ok
    print(f"{parsed.get("count").get_int()!}")    // 3
}

std.log

Structured logging with level filtering.

import std.log

Log Levels

enum Level {
    Debug
    Info
    Warn
    Error
}

Output goes to stderr with timestamps in millisecond precision.

Functions

debug

log.debug(message: string)

Logs at DEBUG level.

info

log.info(message: string)

Logs at INFO level.

warn

log.warn(message: string)

Logs at WARN level.

log_error

log.log_error(message: string)

Logs at ERROR level. Named log_error to avoid conflict with the error keyword.

set_level

log.set_level(level: log.Level)

Sets the minimum log level. Messages below this level are silently dropped.

get_level

log.get_level() log.Level

Returns the current minimum log level.

Example

import std.log

fn main() {
    log.set_level(log.Level.Info)
    log.debug("this is suppressed")
    log.info("application started")
    log.warn("disk space low")
    log.log_error("connection failed")
}

std.math

Integer and float math utilities. Built-in float operations (sqrt, sin, cos, floor, etc.) are available without importing this module.

import std.math

Integer Functions

abs

math.abs(x: int) int

math.abs(-5)    // 5
math.abs(3)     // 3

min / max

math.min(a: int, b: int) int
math.max(a: int, b: int) int

math.min(3, 7)    // 3
math.max(3, 7)    // 7

clamp

math.clamp(x: int, lo: int, hi: int) int

Constrains x to the range [lo, hi].

math.clamp(5, 0, 10)      // 5
math.clamp(-3, 0, 10)     // 0
math.clamp(15, 0, 10)     // 10

pow

math.pow(base: int, exp: int) int

Integer exponentiation. Returns 0 for negative exponents.

math.pow(2, 10)    // 1024
math.pow(3, 3)     // 27

sign

math.sign(x: int) int

Returns 1, 0, or -1.

math.sign(42)     // 1
math.sign(0)      // 0
math.sign(-7)     // -1

gcd / lcm

math.gcd(a: int, b: int) int
math.lcm(a: int, b: int) int

math.gcd(12, 8)    // 4
math.lcm(4, 6)     // 12

factorial

math.factorial(n: int) int

math.factorial(5)    // 120

is_even / is_odd

math.is_even(n: int) bool
math.is_odd(n: int) bool

math.is_even(4)    // true
math.is_odd(3)     // true

Float Functions

clamp_float

math.clamp_float(x: float, lo: float, hi: float) float

math.clamp_float(1.5, 0.0, 1.0)    // 1.0

to_radians / to_degrees

math.to_radians(degrees: float) float
math.to_degrees(radians: float) float

math.to_radians(180.0)    // 3.14159...
math.to_degrees(3.14159265358979323846)    // 180.0

Constants

math.PI() float      // 3.14159265358979323846
math.E() float       // 2.71828182845904523536
math.TAU() float     // 6.28318530717958647692

Note: These are functions that return the constant values.

Example

import std.math

fn main() {
    let n = -42
    print(f"{math.abs(n)}")             // 42
    print(f"{math.clamp(n, 0, 100)}")   // 0
    print(f"{math.gcd(48, 18)}")        // 6
    print(f"{math.factorial(6)}")       // 720
}

std.net

TCP networking: server and client sockets.

import std.net

TcpListener and TcpConnection are objects — entities owning OS resources (a bound port, a live socket). They compare by identity, are shared (not deep-copied) across spawn — handing a listener to a task never forks the descriptor — and their methods serialize per instance, so concurrent users of one connection cannot interleave mid-read or mid-write. See Objects and Entities.

TCP Server

listen

net.listen(host: string, port: int) TcpListener

Binds a TCP server socket. Use port 0 for an OS-assigned port.

TcpListener

let server = net.listen("127.0.0.1", 0)
print(f"Listening on port {server.port()}")

while true {
    let conn = server.accept()
    let data = conn.read(4096)
    conn.write(f"echo: {data}")
    conn.close()
}

TCP Client

connect

net.connect(host: string, port: int) TcpConnection

Opens a TCP connection to the given host and port.

TcpConnection

let conn = net.connect("127.0.0.1", 8080)
conn.write("hello")
let response = conn.read(4096)
print(response)
conn.close()

Example: Echo Server

import std.net

fn main() {
    let server = net.listen("127.0.0.1", 8080)
    print(f"Echo server on port {server.port()}")

    while true {
        let conn = server.accept()
        let msg = conn.read(4096)!
        conn.write(msg)
        conn.close()
    }
}

std.path

File path manipulation utilities. Pure string operations – no filesystem access.

import std.path

Functions

join

path.join(base: string, rel: string) string

Joins two path segments with /.

path.join("/home", "user")    // "/home/user"
path.join("/home/", "user")   // "/home/user"

basename

path.basename(p: string) string

Returns the last component of the path.

path.basename("/home/user/file.txt")  // "file.txt"

dirname

path.dirname(p: string) string

Returns the directory portion of the path.

path.dirname("/home/user/file.txt")  // "/home/user"

ext

path.ext(p: string) string

Returns the file extension including the dot, or empty string if none.

path.ext("file.txt")     // ".txt"
path.ext("Makefile")     // ""

split_ext

path.split_ext(p: string) string

Returns the filename without the extension.

path.split_ext("file.txt")  // "file"

is_absolute

path.is_absolute(p: string) bool

Returns true if the path starts with /.

has_trailing_slash

path.has_trailing_slash(p: string) bool

Returns true if the path ends with /.

normalize

path.normalize(p: string) string

Normalizes a path by resolving . and .. components and removing duplicate slashes.

path.normalize("/home/user/../admin/./docs")  // "/home/admin/docs"

Example

import std.path

fn main() {
    let p = "/home/user/documents/report.pdf"
    print(f"Dir: {path.dirname(p)}")
    print(f"File: {path.basename(p)}")
    print(f"Ext: {path.ext(p)}")
}

std.random

Pseudorandom number generation.

import std.random

Functions

next

random.next() int

Returns a random integer (full range).

between

random.between(low: int, high: int) int

Returns a random integer in [low, high] (inclusive).

let die = random.between(1, 6)

decimal

random.decimal() float

Returns a random float in [0.0, 1.0).

decimal_between

random.decimal_between(low: float, high: float) float

Returns a random float in [low, high).

let temp = random.decimal_between(36.0, 38.0)

coin

random.coin() bool

Returns true or false with equal probability.

seed

random.seed(s: int)

Seeds the random number generator. Same seed produces the same sequence, useful for reproducible tests.

random.seed(42)
let a = random.next()
random.seed(42)
let b = random.next()
// a == b

Example

import std.random

fn main() {
    // Roll 5 dice
    let mut i = 0
    while i < 5 {
        print(f"Roll: {random.between(1, 6)}")
        i = i + 1
    }

    // Reproducible sequence
    random.seed(99)
    let x = random.between(1, 100)
    let y = random.between(1, 100)
    print(f"Seeded: {x}, {y}")
}

std.regex

Simple pattern matching. Supports literals, . (any character), ^/$ anchors, */+/? quantifiers on a single token, the classes \d (digit), \w (letter, digit or _) and \s (space, tab, newline), and \x for a literal metacharacter (\., \*, \\). No alternation, groups or bracket classes.

import std.regex

Functions

matches

regex.matches(pattern: string, text: string) bool

Returns true if the pattern matches anywhere in the text.

regex.matches("he..o", "hello")  // true
regex.matches("^hi", "hello")   // false

find

regex.find(pattern: string, text: string) int

Returns the index of the first match, or -1 if not found.

find_all

regex.find_all(pattern: string, text: string) [int]

Returns an array of all match start positions.

replace

regex.replace(pattern: string, replacement: string, text: string) string

Replaces the first match with the replacement string.

regex.replace("world", "pluto", "hello world")  // "hello pluto"

replace_all

regex.replace_all(pattern: string, replacement: string, text: string) string

Replaces all matches with the replacement string.

split

regex.split(pattern: string, text: string) [string]

Splits the text at each match of the pattern.

regex.split(",", "a,b,c")  // ["a", "b", "c"]

Example

import std.regex

fn main() {
    let text = "The quick brown fox"
    if regex.matches("qu..k", text) {
        print("Found a match")
    }
    let cleaned = regex.replace_all(" +", " ", "too   many   spaces")
    print(cleaned)
}

std.rpc

HTTP-based RPC client for cross-stage method calls. Used internally by the compiler-generated RPC stubs.

import std.rpc

Functions

http_post

rpc.http_post(url: string, body: string) string

Sends an HTTP POST request with a 5-second timeout. Returns the response body.

http_post_with_timeout

rpc.http_post_with_timeout(url: string, body: string, timeout_ms: int) string

Sends an HTTP POST request with a custom timeout in milliseconds.

std.socket

Low-level TCP socket operations. For higher-level HTTP, use std.http or std.net.

import std.socket

Functions

create

socket.create(domain: int, sock_type: int, protocol: int) int

Creates a socket and returns a file descriptor. Use domain 2 (AF_INET), sock_type 1 (SOCK_STREAM), protocol 0.

bind

socket.bind(fd: int, host: string, port: int) int

Binds a socket to an address and port.

listen

socket.listen(fd: int, backlog: int) int

Marks a socket as listening for incoming connections.

accept

socket.accept(fd: int) int

Accepts a connection and returns a new file descriptor for the client.

connect

socket.connect(fd: int, host: string, port: int) int

Connects to a remote host.

read

socket.read(fd: int, max_bytes: int) string

Reads up to max_bytes from a socket.

write

socket.write(fd: int, data: string) int

Writes data to a socket. Returns number of bytes written.

read_bytes / write_bytes

socket.read_bytes(fd: int, max_bytes: int) bytes
socket.write_bytes(fd: int, data: bytes) int

Binary-safe variants of read and write. read_bytes returns empty bytes on EOF or error.

set_read_timeout / read_timed_out

socket.set_read_timeout(fd: int, ms: int) int
socket.read_timed_out() int

set_read_timeout sets a read deadline (SO_RCVTIMEO): later reads block at most ms milliseconds, and ms <= 0 clears it. After a read comes back empty, read_timed_out() returns 1 if the deadline elapsed and 0 for EOF or a connection error.

close

socket.close(fd: int) int

Closes a socket.

set_reuseaddr

socket.set_reuseaddr(fd: int) int

Sets the SO_REUSEADDR option on a socket.

get_port

socket.get_port(fd: int) int

Returns the port number a socket is bound to.

Example

import std.socket

fn main() {
    let fd = socket.create(2, 1, 0)
    socket.set_reuseaddr(fd)
    socket.bind(fd, "0.0.0.0", 8080)
    socket.listen(fd, 128)
    print("Listening on :8080")
    let client = socket.accept(fd)
    let data = socket.read(client, 4096)
    print(f"Received: {data}")
    socket.close(client)
    socket.close(fd)
}

std.strings

String utility functions. Pluto strings are immutable; all operations return new strings.

import std.strings

Functions

substring

strings.substring(s: string, start: int, length: int) string

Returns length characters starting at byte offset start.

strings.substring("hello, world", 0, 5)     // "hello"
strings.substring("hello, world", 7, 5)     // "world"

contains

strings.contains(s: string, needle: string) bool

strings.contains("hello world", "world")    // true
strings.contains("hello world", "xyz")       // false

starts_with / ends_with

strings.starts_with(s: string, prefix: string) bool
strings.ends_with(s: string, suffix: string) bool

strings.starts_with("hello", "hel")    // true
strings.ends_with("hello", "llo")      // true

index_of

strings.index_of(s: string, needle: string) int

Returns the byte offset of the first occurrence, or -1 if not found.

strings.index_of("hello", "ll")     // 2
strings.index_of("hello", "xyz")    // -1

trim

strings.trim(s: string) string

Strips leading and trailing whitespace.

strings.trim("  hello  ")    // "hello"

trim_start / trim_end

strings.trim_start(s: string) string
strings.trim_end(s: string) string

Strip whitespace from one end only.

strings.trim_start("  hi  ")    // "hi  "
strings.trim_end("  hi  ")      // "  hi"

to_upper / to_lower

strings.to_upper(s: string) string
strings.to_lower(s: string) string

strings.to_upper("hello")    // "HELLO"
strings.to_lower("HELLO")    // "hello"

Only ASCII letters change case; every other character is copied unchanged.

replace

strings.replace(s: string, old: string, new_str: string) string

Replaces all occurrences of old with new_str.

strings.replace("hello world", "world", "pluto")    // "hello pluto"

split

strings.split(s: string, delim: string) [string]

Splits into an array by delimiter.

let parts = strings.split("a,b,c", ",")
// ["a", "b", "c"]

join

strings.join(arr: [string], sep: string) string

Joins an array of strings with a separator.

strings.join(["a", "b", "c"], ", ")    // "a, b, c"

char_at

strings.char_at(s: string, index: int) string

Returns the character at byte offset index as a single-character string.

strings.char_at("hello", 0)    // "h"
strings.char_at("hello", 4)    // "o"

byte_at

strings.byte_at(s: string, index: int) int

Returns the raw byte value at the given offset.

strings.byte_at("A", 0)    // 65

len

strings.len(s: string) int

Returns the byte length of the string. Equivalent to s.len().

strings.len("hello")    // 5

format_float

strings.format_float(v: float) string

Formats a float as a string with decimal representation.

last_index_of

strings.last_index_of(s: string, needle: string) int

Returns the index of the last occurrence of needle, or -1 if absent.

strings.last_index_of("a/b/c", "/")    // 3

count

strings.count(s: string, needle: string) int

Counts non-overlapping occurrences of needle.

strings.count("banana", "an")    // 2

is_empty / is_whitespace

strings.is_empty(s: string) bool
strings.is_whitespace(s: string) bool

is_empty is true for "". is_whitespace is true when the string is empty or contains only whitespace.

repeat

strings.repeat(s: string, count: int) string

Concatenates count copies of s; 0 or less gives "".

strings.repeat("ab", 3)    // "ababab"

compare

strings.compare(a: string, b: string) int

Lexicographic byte-wise comparison: -1 if a sorts first, 0 if equal, 1 if a sorts after b. A proper prefix sorts first, and bytes compare unsigned, so for UTF-8 text this is code-point order.

strings.compare("ab", "abc")    // -1
strings.compare("b", "a")       // 1

parse_int / parse_float

strings.parse_int(s: string) int       // raises strings.ParseError
strings.parse_float(s: string) float   // raises strings.ParseError

Strict parsers that raise ParseError { input, message } instead of returning none (compare s.to_int() / s.to_float()). parse_int accepts an optional sign and ASCII digits over the full int range, and rejects whitespace anywhere (trim first for padded input) and out-of-range values. parse_float accepts [+-]? DIGITS ('.' DIGITS)? ([eE] [+-]? DIGITS)?; .5, 5., inf, nan and values too large for a finite float are rejected.

let n = strings.parse_int("-42")!          // -42
let x = strings.parse_float("2.5e-3")!     // 0.0025
let bad = strings.parse_int(" 7") catch err: strings.ParseError {
    print(err.message)                     // invalid character at index 0
    0
}

Example: CSV Parsing

import std.strings

fn main() {
    let line = "Alice,30,Engineering"
    let fields = strings.split(line, ",")
    let name = fields[0]
    let dept = strings.to_upper(fields[2])
    print(f"{name} works in {dept}")
    // Alice works in ENGINEERING
}

std.time

Wall-clock time, monotonic time, and sleep.

import std.time

Functions

now / now_ns

time.now() int       // wall-clock milliseconds since Unix epoch
time.now_ns() int    // wall-clock nanoseconds since Unix epoch

Wall-clock time. Subject to system clock adjustments. Use for timestamps, not benchmarking.

monotonic / monotonic_ns

time.monotonic() int       // monotonic milliseconds
time.monotonic_ns() int    // monotonic nanoseconds

Monotonically increasing clock. Never goes backwards. Use for measuring elapsed time.

sleep

time.sleep(ms: int)

Blocks the current thread for at least ms milliseconds.

elapsed

time.elapsed(start_ms: int) int

Returns monotonic() - start_ms. Convenience for timing blocks of code.

Example: Benchmarking

import std.time

fn main() {
    let wall = time.now()
    print(f"Unix timestamp (ms): {wall}")

    let start = time.monotonic()
    time.sleep(100)
    let ms = time.elapsed(start)
    print(f"Slept for {ms}ms")
}

std.uuid

UUID v4 generation.

import std.uuid

Functions

generate

uuid.generate() string

Returns a random UUID v4 string in standard format: xxxxxxxx-xxxx-4xxx-yxxx-xxxxxxxxxxxx.

let id = uuid.generate()
// e.g. "a3b4c5d6-1234-4abc-9def-0123456789ab"

Example

import std.uuid

fn main() {
    let id1 = uuid.generate()
    let id2 = uuid.generate()
    print(f"ID 1: {id1}")
    print(f"ID 2: {id2}")
}

std.wire

Wire format for serializing Pluto values. Used internally by the RPC system to marshal data across service boundaries.

import std.wire

Types

WireValue

An enum representing any serializable value:

enum WireValue {
    Int { value: int }
    Float { value: float }
    Bool { value: bool }
    Str { value: string }
    Array { elements: [WireValue] }
    Record { keys: [string], values: [WireValue] }
    Variant { name: string, data: WireValue }
    Null
}

WireError

error WireError {
    message: string
}

Raised on type mismatches during decoding.

Factory Functions

wire.wire_int(v: int) WireValue
wire.wire_float(v: float) WireValue
wire.wire_bool(v: bool) WireValue
wire.wire_string(v: string) WireValue
wire.wire_bytes(v: bytes) WireValue
wire.wire_array(elems: [WireValue]) WireValue
wire.wire_record(keys: [string], values: [WireValue]) WireValue
wire.wire_variant(name: string, data: WireValue) WireValue
wire.wire_null() WireValue

Traits

Encoder / Decoder

Traits for implementing custom wire formats. Methods for encoding/decoding each primitive type, arrays, maps, records, and variants.

WireFormat

trait WireFormat {
    fn serialize(self, value: WireValue) string
    fn deserialize(self, data: string) WireValue
}

Built-in Implementations

JsonWireFormat

JSON-based wire format. Create with wire.json_wire_format().

let fmt = wire.json_wire_format()
let encoded = fmt.serialize(wire.wire_int(42))
let decoded = fmt.deserialize(encoded)

WireValueEncoder / WireValueDecoder

Streaming encoder/decoder for building WireValue trees. Create with wire.wire_value_encoder() and wire.wire_value_decoder(value).