What a function may do belongs in its type.

fn load_config() {
    read_file("ops.toml");        // reaches the filesystem
}

$ buildc check missing_effect.bld
function `load_config` performs effect `FileSystem` but does not declare it
  help: add ~ FileSystem to the signature
  note: capability `FileSystem` was triggered by ambient call(s): read_file

# declare the effect, and the same check passes, then writes a receipt
fn load_config() ~ FileSystem { read_file("ops.toml"); }

$ buildc check load_config.bld --receipt receipt.json
Type checking... OK
  "declared_effects":      { "load_config": ["FileSystem"] }
  "observed_capabilities": { "load_config": { "FileSystem": ["read_file"] } }

Touch your files without saying so, and it won’t build; the error points at the exact line that did it. Declare it instead, and it passes, and the compiler writes down what you promised, right next to what it actually saw you do.

Captured live from buildc check (Rust toolchain, release build) · the effect is built into the function and checked every time it’s called. That little receipt is the heart of it (what you promised, side by side with what really happened), and it’s honest that this is the foundation, not a finished, ship-it-tomorrow product.

fn pick<'a, 'b>(x: &'a i32, y: &'b i32) -> &'a i32 {
    y          // returns 'b where the signature promised 'a
}

$ buildc check pick.bld
Lexing... OK (28 tokens)
Parsing... OK (1 items)
Type errors found:
  function returns `&'b i32` but expected `&'a i32`

Here’s what’s happening: the function promised to hand back one specific piece of memory, then tried to hand back a different one that might disappear sooner. The compiler catches the swap and says no. How long memory is allowed to live is a promise too, and it’s kept.

Diagnostic from compiler/src/types/error.rs, surfaced through the lifetime matching in unify.rs. An honest limit, said plainly: this memory-lifetime checking is not yet complete. It already follows memory as it passes between functions (that’s the Phase 1 work), but I haven’t finished proving every case at the caller’s side, so I won’t claim it’s complete.

# an algebraic effect with a handler: parsed, effect-checked,
# lowered to C, compiled, and run:
$ buildc run examples/quickstart/effects_greeting.bld
Hello, teammate!

That same promise-keeping follows the program the whole way down: read it, check what it’s allowed to touch, translate it into the C language, and run it. From there, one path turns it into a real program your machine can run on its own.

The C path is the one that works start to finish, and the tests prove it. The others (LLVM, WASM, SPIR-V, x86-64, ARM64, and a route that writes Rust) can produce code, but they’re still experiments. I’d rather just tell you that than let you assume otherwise.

# name a C library by its header and link flag, then call straight in:
extern "C" link "sqlite3" header "<sqlite3.h>" {
    fn sqlite3_libversion() -> &str;      // the header stays authoritative
}
fn main() ~ Foreign { let v = sqlite3_libversion(); }

$ buildc build examples/ffi --emit c
[4/4] Code generation (c)... OK (53517 bytes)

# in the emitted C, verbatim:
#include <sqlite3.h>          // your header, included as-is
// buildc-link: sqlite3       // recorded, so `buildc build` links it
_1 = sqlite3_libversion();    // the real call into the C library

# the reverse is `extern "C" fn` (C calls BuildLang). and a live run
# straight through a C variadic:
$ buildc run examples/variadic/main.bld
the answer is 1 and 2

Name a C library by its header and link flag, and BuildLang includes the header, records the link, and calls straight in. extern "C" fn goes the other way, so C can call back. A foreign call is still an effect: main declares ~ Foreign, so reaching into C sits behind the same check as touching a file.

Captured live from buildc build --emit c and buildc run (release build). buildc emits the include, the link directive, and the call, checked end to end through the build; the final native link against sqlite3 is your own C toolchain’s job, not something the test suite claims for you.

# a heat-diffusion kernel: its energy should never climb. run it,
# check the invariant, seal a receipt:
$ buildc run heat.bld --emit-receipt heat.json --invariant energy-monotone
Running... OK (240 steps captured)
Invariant energy-monotone... HELD
  "label":     "NOT_A_NEW_PHYSICAL_LAW"
  "verdict":   "HELD"   // witnesses the OUTPUT SERIES, not the PDE

# re-run from scratch and re-derive the verdict. change a number and it fails:
$ buildc receipt verify heat.json
Re-running program... OK
Re-deriving verdict... MATCH       # drift / tamper / source-change each fail typed

The receipt doesn’t ask you to trust a stored answer. Verify re-runs the program and works the verdict out again, so a nudged number, an edited receipt, or a changed source can’t slip through, each trips its own named failure.

Captured live from buildc run --emit-receipt and buildc receipt verify (release build) · the JSON is re-checkable and every receipt is stamped NOT_A_NEW_PHYSICAL_LAW. The plain limit: this witnesses the compiled program’s observed output series against a stated rule; it does not prove the equations, and buildc is not a finished replacement for Julia.

# every invariant ships paired: a kernel that should HOLD and one that
# should VIOLATE, so a verdict of HELD actually means something.
energy-monotone    # the series never climbs past tolerance
conservation       # stays within roundoff of its starting value
bounded            # never exceeds the initial value (a discrete maximum principle)
energy-identity    # per-step energy balance holds to roundoff
                   // the FTCS analogue of d/dt ∫u² = -2a ∫u_x²
relation --columns N  # N reported columns must agree, so a run can't hide a divergence
conserved-band     # approximate conservation inside a fixed error budget

# conserved-band grounds symplectic integration, and it shows the point:
$ buildc run leapfrog.bld --emit-receipt lf.json --invariant conserved-band
Invariant conserved-band... HELD    # energy stays in an O(dt²) band
$ buildc run euler.bld    --emit-receipt eu.json --invariant conserved-band
Invariant conserved-band... VIOLATED # explicit Euler drifts out and fails, as it should

A verdict is only worth trusting if it can say no. Each invariant carries a matched pair: a kernel meant to hold and one meant to break, at a fixed tolerance, so a green result is a real result and not a rubber stamp.

Six invariants · energy-monotone, conservation, bounded, energy-identity, relation --columns, and conserved-band, each with paired positive and negative kernels · the leapfrog-versus-Euler contrast is the honest demonstration that conserved-band actually distinguishes a good integrator from a drifting one. Still true here: a receipt witnesses observed output, not a proof of the physics.

# re-verify, then hand witnessed measurements to Crucible (the Telos bridge):
$ buildc receipt export heat.json --to crucible
Re-verifying... OK
Emitting witnessed measurements... OK
  "witnessed": true   // re-derived here, not trusted from the file
  "label":     "NOT_A_NEW_PHYSICAL_LAW"

Export doesn’t forward a stored claim. It re-verifies first, then emits measurements Crucible can stand behind, carrying the same honest label the whole way across.

The backends, said plainly: C is the only production-verified path; HLSL and GLSL cover shaders; SPIR-V, LLVM, WASM, Rust, x86-64, and ARM64 stay experimental. cargo install buildlang is accurate (buildlang 1.1.0 is on crates.io), but the published crate predates this receipt work, so don’t read the newest invariants into the version you install today.