Ownership#

A file, a socket, a C allocation — anything that needs exactly one cleanup — carries that obligation in its type. The checker finds the missing cleanup, the double free, and the use-after-move before the program runs.

The model is deliberately smaller than Rust's: no named lifetimes, no typestate, and no borrow checker over arbitrary object graphs. It is aimed at the failures that happen at a C boundary, and it costs one annotation on the producer.

This page is the working subset. The ownership reference has the complete model.

Declaring a resource#

@drop marks the operation that consumes the resource; @owned marks the function that produces one:

The annotation, rather than the name, is what makes close the drop operation. Bare @owned is accepted only when the result type has exactly one, so the compiler never has to guess between close, free, flush, and stop.

For a type you do not own, the drop operation can be a free function, and the producer names it:

A drop operation must takes its resource. That is what makes it consuming.

Discharging the obligation#

Once you bind an owner, its exact cleanup runs automatically at the binding's lexical boundary:

There are three ways to end or transfer the obligation before that boundary.

Drop it at the point you choose:

Hand it on to a parameter that takes it:

Return it from a function that is itself @owned.

Inside a function, a takes parameter is discharged by passing it to another takes parameter — the drop operation, or something that adopts it. nupp.drop() needs a value whose static type carries a cleanup list, and a bare takes binding does not have one, so nupp.drop(session) there reports NUPP2602 and names the fix.

Borrowing#

A borrows parameter gets access for the duration of the call without taking responsibility:

borrows is a lifetime and aliasing contract rather than a const qualifier — mutating through one is allowed. Use exclusive for a call that needs sole access because it may invalidate views derived from the value.

For a Nupp function with a body, the checker infers whether a resource parameter escapes, so a read-only helper needs no annotation at all. Writing borrows anyway pins the contract: a later change that stores the value errors inside the function instead of silently changing its interface and breaking callers.

A borrow may be read, mutated, and reborrowed. It may not be returned without a contract, stored in a table or field, assigned to an outer binding, or captured by a closure.

Lexical destruction#

Cleanup runs on fallthrough, return, break, continue, a goto leaving the block, and an error raised anywhere inside. Several resources are acquired left to right and released right to left.

The bindings remain owners: they may be moved, returned under an owning contract, or explicitly dropped early. Each successful transfer deactivates automatic cleanup exactly once.

Records that hold resources#

A record with owned<T> fields is itself a resource, and cleanup is synthesized in reverse field order:

A custom @drop method has to discharge every affine field, and it does that by calling their drop operation directly:

Where it stops#

unsafe do grants permission for pointer operations the checker cannot prove — raw dereference, intoRaw, fromRaw, borrowFrom. It grants nothing else: owners still have to be discharged inside one, borrows still cannot escape, and ordinary lexical cleanup still runs.

The trusted parts are written down. Whether a C function really consumes, retains, or releases a pointer comes from its declaration, because a header has no body to inspect. Whether a returned resource is genuinely exclusive is not observable from a pointer value. Cleanup bodies are not verified. Those are the auditable edges; everything inside them is checked.

Next#

• The ownership reference — the complete model, C output parameters, pinning, and the proved-versus-trusted table.
• C interop — parameter modes at a C boundary.