Shape

A checked programming language from input. Contracts and proofs in the source, its own native backend, and a built-in package manager.

See a contract Input

Contracts in the source

fn clamp(value: Int, minimum: Int, maximum: Int) -> Int:
    requires minimum <= maximum
    ensures result >= minimum
    ensures result <= maximum
    if value < minimum:
        minimum
    else:
        if value > maximum:
            maximum
        else:
            value

requires and ensures are part of the function, checked before the program runs and verified on demand.

Contracts

requires and ensures clauses on every function — preconditions, postconditions and invariants, not comments.

Verification

shape verify emits proof certificates; shape proof-check audits them independently of the compiler.

Effects

No ambient authority. io, network, storage, gpu, clock and entropy are declared in the signature and granted at run time.

Native backend

Its own machine-code generator targeting x86-64, AArch64 and RISC-V 64 — plus WebAssembly. No LLVM.

GPU

A first-class gpu effect; std.gpu_* runs compute kernels on device alongside everything else.

Parallelism

std.parallel and the tasks effect run independent computations side by side.

Package manager

shape add, remove and fetch manage dependencies.toml — a plain manifest instead of magic.

Tooling

shape lsp for the editor, shape fix for canonical formatting, shape test for the suite.

Shape is in active development (0.9.0) and not yet ready for production use.