What the program guarantees

Seven claims. Each one carries a snippet the site compiles and runs against this tree on every deploy — a claim whose snippet stops saying it fails the deploy.

claim 01The signature is the receipt

One signature lists every run a function may touch, and those runs are an upper bound. A body that reaches past its receipt does not compile.

snippets/receipt.nib · the receipt is printed before anything runs

the receipt · func greeting : String -> String ! Config

snippets/receipt_lie.nib · the body reaches two runs, the signature admits one exit 1

the refusal · the `!` clause is an upper bound

claim 02Raising is named too

raises is part of the receipt: a missing file is a possible answer, and the caller is told before the call is made. Understate the list and nothing compiles.

snippets/raises.nib · raises FileNotFound is in the signature exit 1

the receipt, then the run · FileNotFound("/nonexistent/nib-site-demo…")

snippets/raises_lie.nib · the body raises FileNotFound, the signature admits IndexOutOfRange exit 1

the refusal · `raises` is an upper bound in exactly the same way

claim 03Keeping code is spelt `pin`

A var holds its value for as long as the instance exists, so keeping code there has to be written down in the type. A plain arrow means the value is lent; pin means it may outlive the call.

snippets/loan_plain.nib · code kept in a plain-arrow var exit 1

the refusal · storage is exactly what that promise denies

snippets/loan_pin.nib · the same field, one word exit 0

the run · the intention is visible in the type

claim 04A loan reaches into module bodies

An arrow-typed parameter is lent for the duration of the call: the body may apply it and nothing else. Handing it onward is refused unless the parameter says pin.

snippets/loan_handoff.nib · a lent parameter handed to a pin parameter exit 1

the refusal · write the parameter `pin (…) -> …` if the body must keep it

snippets/loan_handoff_pin.nib · same body, one word exit 0

the run · every caller knows it is handing over a pin

claim 05Cross-cutting is a second effector

A wrapper is not a decorator or an annotation: it is another instance, forwarding. Kit.Plain |> Kit.Counted answers the same interface and the run prints 41 instead of 40.

snippets/wrapper.nib · an effector whose payload is another effector

two runs · wire Bare prints 40, wire Wrapped prints 41

claim 06A record is what an interface asks for

No interface declaration, no is, no registration: a record is accepted where Iter.Enumerable<String> is wanted because it has the one operation that interface asks for.

snippets/structural.nib · nothing had to be registered anywhere

the run · Iter counted 3 rows

claim 07Concurrency claims are refused

concurrent marks a lane nothing runs, so a mutable field there is refused at compile time rather than accepted and quietly wrong. Declare the effector sequential — the only mode with a lifecycle.

snippets/concurrent_var.nib · a var in a concurrent effector exit 1

the refusal · a claim about concurrency the runtime does not keep

what it is not → the tour → back home