hanki

6. Effects

Effects are typed markers, checked statically. They are not algebraic: there is no handle or with, and io.print! cannot be intercepted at runtime.

Built-in effects:

EffectMeaning
[io]standard input/output
[net]network access
[fs_read]reading the filesystem
[fs_write]writing the filesystem
[db]embedded database access (see stdlib/extra/sqlite.hk); covers :memory: databases too
[process]subprocess spawn (see stdlib/extra/process.hk)
[time]reading the clock / sleeping
[env]environment-variable reads
[random]random-number generation
[throws E]may throw an error of type E
[state]inside an actor handler; reads/writes actor state
[local]mutation of state the computation owns; implicit in every action's row, writable only on a function type (see Non-substitutability in the row)
[runtime_state]observing process-global state the program does not own; on log.min_level! / log.set_min_level! / log.enabled! and viral through their callers

Multiple effects: [io, throws ParseError].

A row is a set. [io, db] and [db, io] are one type, the order you write means nothing, and hanki fmt canonicalizes a row the way it canonicalizes an import block. The bare tags come first, sorted alphabetically and case-insensitively; user-defined effects are capitalized, and a byte ordering would cluster every one of them ahead of the built-ins. Then Crash, then each throws E, then the effect variable (below). Those last three are what a reader scans a row for, can this diverge, must I handle a throw, is the row still open, and they take the tail in place of sorting in among the tags. [io, fs_read, Crash] prints as [fs_read, io, Crash], and [e, net] as [net, e].

[fs] is an alias for [fs_read, fs_write], sugar you may write in an effect row or an --allow/--deny atom, expanded to the two base atoms wherever effect names are interned. --allow fs_read grants a read-only filesystem and refuses a writer, and [fs] on an action that both reads and writes declares both.

User-defined effect groups:

struct Rows
  affected: i32
end

effect Database
  def query(sql: string) -> Rows
  def exec(sql: string) -> ()
end

The built-in names above are reserved. An effect block may not take one of them, the nine capability atoms, the [fs] alias, state, local, runtime_state or Crash. Effect names are one flat vocabulary: a same-named user effect would merge with the builtin in place of shadowing it, and --allow io would then grant both with no way to say which was meant (H0632).

The ops inside an effect block are declared as def, with no ! and no body; they are signatures. At a call site they implicitly charge the [Name] effect, and the caller must declare it:

def run!() -> () [Database]
  exec("DELETE FROM things")    # legal: caller has [Database]
end

An op is bare-callable only within its declaring module, or where that module is opened. Like every other top-level name it sits at its module-qualified name (§14) and is never a bare global that could collide with or shadow a same-named identifier in a file that did not open it, which matters where the stdlib is merged into every program. An op is never reachable as module.op: that spelling would make an op call read like an ordinary action call while hiding the atom it charges. Its qualified spelling goes through the effect's name:

Database.exec("DELETE FROM things")      # effect name in scope (declaring module, or `open db`)
db.Database.exec("DELETE FROM things")   # under `use db`

The call form therefore spells the atom it charges, in call and value position alike, and f = db.Database.exec stores the op as readily as f = exec does inside its own module. The two spellings are the same reference as the bare one, with identical row charging, purity wall, provider binding and behaviour on both tiers. Only the spelling differs, and db.exec(…) remains an error naming both forms that work. Within its own module an op call is bare (exec(…) above), as is the matching provide op name. A use is kept live by the qualified spelling like any other qualified reference. An op whose name starts with _ remains private to its module through it (§12). Where a module declares an effect Foo beside a type Foo, Foo.member searches both namespaces, and a member both supply is an error and no silent pick (H0633, the §14 composition rule).

An effect block gives its ops signatures and no behavior. A provide block binds the implementations:

provide Database [net]
  def query(sql: string) -> Rows
    Rows(affected=0i32)          # ordinary action body; its budget is [net]
  end
  def exec(sql: string) -> ()
    ()
  end
end

Rifts: answering an effect with Rust

A provide block answers an effect with Hanki. An application may answer one with native code: a Rust crate in its own repository, bound by its manifest, reached through the effect's ops the way a Hanki provider is. That opening is a rift, and a program opens one. It is how a program reaches a library the stdlib does not wrap, such as Steamworks, a physics engine, an audio backend or a codec, with no feature request per library.

Only an application root may open one, never a package at any depth (§17, invariant 1). A dependency that tries is refused at resolution (H0641). A rift is therefore first-party: it sits in the repository of the program it serves, written by the same author, and no dependency can introduce one, ask for one, or tell whether one is present.

The effect declaration is the whole FFI signature: the same block a provide would satisfy, with no extern and no pointer type added to the language:

# audio.hk - the interface, ordinary Hanki
struct Clip
  id: i64
  gain: f64
end

effect Audio
  def play(clip: Clip) -> Result<(), AudioError>
  def stop() -> ()
end

hanki rift new audio.Audio native/audio scaffolds the crate and writes the api crate it compiles against. The author implements one generated trait with ordinary Rust and exports pub fn open() -> impl Audio. The manifest binds it (§21), and hanki run and hanki build regenerate and build it: loaded beside the program on the bytecode tier, linked into the binary by hanki build, which also links whatever the crate's own build.rs asks for. The Rust author writes no unsafe, sees no Hanki heap, and cannot call back into Hanki.

HankiRustNotes
() bool() bool
i8…i64 / u8…u64the same width
f32 / f64f32 / f64IEEE bits; an f32 signalling NaN comes back quiet, since the runtime's float slot is an f64
stringStringUTF-8 validated on the way back
bytesVec<u8>
Option<T> / Result<T, E>the samea fallible op is declared Result; ops have no throws
List<T>Vec<T>
Pair<A, B>(A, B)
non-generic struct / sum typepub struct / pub enumfields and variants in declaration order

Everything else is a compile error at the binding (H0639) naming the op, the parameter or return, and the type: int, decimal and rational (unbounded, and with in-band sentinels; declare a fixed width, or convert in an adaptor provide), Map (its trie is a private stdlib representation the runtime cannot enumerate; cross a List<Pair<K, V>>), resources, Future<T>, function types, ActorRef<T>, and generic user types. Every op, parameter, field, variant and type name must also have a Rust spelling of its own (H0643). A predicate's ? is dropped, a Rust keyword is raw-escaped, and self, Self, crate and super, or two names that collide once the ? goes, are refused, as is a user type whose name is one the generated crate already spells: Vec, Result, String, its own Wire or DecodeError, or the trait the effect's own name becomes.

The design record is docs/design/native-rifts.md; the manifest surface is §21.

A function that performs whatever its callback performs is polymorphic in that callback's effects. Write the row as a single lowercase letter, an effect variable, in the callback's type, and again in the function's own row:

def apply_twice!(x: T, f: (T) -> () [e]) -> () [e]
  f(x)
  f(x)
end

e stands for whatever effects the callback performs. A single lowercase letter is an effect variable as a single uppercase letter is a type parameter (§11); built-in effects like io are multi-letter, and the two never collide. Invoking f in the body charges [e], which apply_twice! declares. At each call site e is solved to the concrete effects of the callback passed for f and folded into the caller's required set. Passing a closure that performs [io] charges the caller [io], and a pure callback charges nothing. A row may combine concrete effects with a variable, -> () [fs, e], meaning "I touch the filesystem, plus whatever the callback does". A variable may be forwarded: a higher-order action can pass its [e] callback on to another [e] action, and the row remains open until the outermost call site.

A bound may name a row too. A callback is not the only thing whose effects a signature can be polymorphic in. A trait method may declare its row as a variable, each impl answers it with a concrete row of its own, and a bounded generic names that row through its bound:

trait Stream
  def read!(self, max: u32) -> bytes [e]
end

impl Stream<TcpStream>
  def read!(self, max: u32) -> bytes [net]
  # ...
end

impl Stream<MemStream>
  def read!(self, max: u32) -> bytes
  # ...
end

def read_head!<S: Stream[e]>(s: S, max_head: int) -> Result<Head, HttpError> [e]
  # `s.read!(...)` charges `[e]`, which this signature declares
end

The variable is bound by the generic-param list and rigid inside the body, as a callback's is. A multi-bound parameter brackets only the bounds that name one (<S: Stream[e] + Display>), and two bounds get two variables (<S: Stream[e], T: Sink[r]> … [e, r]). At each call site the variable solves to the union of the impl's rows for every method the trait declares with a variable row, and never to the subset the body happens to call. A caller reading <S: Stream[e]> can therefore say what e is from the signature alone. read_head!(tcp) charges [net], and read_head!(mem) charges nothing beyond local. A generic that forwards its own still-generic S to another leaves the variable unsolved, and the outermost concrete instantiation closes it.

Bound effect rows resolve after argument and result type inference, including numeric literal defaults. When a row variable is shared by bounds and callbacks, each call requires the union of all selected implementation rows and callback rows. This also applies to saved function values and higher-order arguments; their callback rows are solved separately at each invocation. Row names are local to each signature, and forwarding preserves independent caller rows even when a callee uses the same letters. A parameterized bound selects its implementation with the complete type argument tuple after expanding trailing defaults.

Four rules fence it, each with its own diagnostic. A trait method's row is either concrete or one variable; [net, e] is refused (H0647), a mixed row stating a floor under the ceiling every other row states. An impl answers a variable row with a concrete row, a variable there having nothing to solve it (H0648). A bound may name a row only where the trait, or a trait above it, leaves one open, and the bracket takes one variable and no more (H0649). Calling a variable-row method through a bound that did not name the row is refused (H0650) in place of charging an atom the signature cannot name. Forwarding a generic argument to a callable whose bound names a row also requires that row on the enclosing bound (H0650), even when an unrelated callback happens to use the same letter. Under a concrete trait row nothing changes: an impl may perform fewer effects than the trait declares and never more (§10, H0617). Design: docs/design/trait-effect-rows.md.

A function type may take an effect row after its return type, as a def does: (T) -> () [io], (string) -> i32 [throws ParseError]. The row is the effects a value of that type performs when called. It matters wherever a function is stored or returned in place of invoked on the spot: a struct field, an annotated let, a function's return type.

struct Event
  name: string
end

struct Handlers
  on_event: (Event) -> () [io]   # calling on_event performs [io]
end

A variable row is no concrete contract. A value whose type has an effect variable may be invoked in place or forwarded to another polymorphic parameter. It cannot be stored in a struct field, returned through a concrete return type, or bound to an annotated let; those slots demand a fixed row. Storing one is a compile error: a polymorphic callback can perform anything, and a later invocation from a pure or under-declared context would launder its effects. Use a concrete row ([io]) to store a real callback, and the variable to call or forward it.

The package-manifest wire format encodes these rows on function-typed components of an exported signature, and the load-time compatibility check (module.load!) compares them. A callback slot's effects are therefore enforced across a shared-module boundary. Source-level cross-package import reconstructs an imported signature by re-parsing and re-checking the dependency's cached source. hanki build resolves each declared universe dep into the content-addressed cache and binds use <alias> to that package's cached <alias>.hk module, and callers are checked against the dependency's real definitions; a fetched universe dep is inert source with no .hanki_manifest. Resolution is transitive: a resolved dependency's own manifest resolves too, and its own use binds its declared deps. Each package sees only its own manifest's aliases and never the consuming project's, and a dependency's non-sibling use of an undeclared name remains an unresolved-import error in place of a silent reach into the project's deps. One version per source applies graph-wide (§21). Known limitation (tracked): as elsewhere in the manifest, a throws E payload is compared by name only (throws) and not by error type.

Encapsulated purity: @encapsulated

! has two distinct meanings. A world effect, a non-empty row over io/fs/net/db/process/time/env/random/throws E/Crash, is a real observable interaction. An action with an empty effect row takes its ! for the other reason: it is not substitutable. BytesBuilder.push! mutates a builder, and a BytesReader read advances a cursor (§4). Neither is a world effect, two calls still differ, and the operation takes the !. A pure def cannot call any !, and this second class infects pure contexts (meta, where-invariants, content-hashing) even for code that is externally pure: a local builder created, written and finalized inside a function never escapes, and the function is a pure function of its inputs.

@encapsulated is a def-level attribute marking a def, with no ! and externally pure, that may call empty-effect-row actions internally. The checker proves external purity from three rules and trusts nothing:

  1. Empty-effect-row actions only. The body may call !-actions whose row is empty. Any call to an action with a non-empty row, or any throw, is a compile error (H0607). The encapsulated def's own row is therefore empty: it performs no side effect, throw or crash. World-effect safety is untouched, and no route launders one.
  2. No mutable inputs (H0609). Every parameter, self included, must be deeply immutable, on the same lattice as rule 3. A def cannot capture an enclosing binding and there is no ambient global mutable state, and immutable parameters therefore guarantee that every mutable value the body touches was allocated inside the function. The body can only mutate local state. A foreign mutable is rejected outright and never origin-tracked, since even reading one, advancing a cursor, is non-substitutable. A helper that mutates a passed-in builder is therefore an ordinary empty-effect-row action, and the @encapsulated boundary sits at the entry point that owns the builder. A generic parameter is checked where it is instantiated and not where it is declared (H0629, reported at the call): v: T cannot say what T will become, a caller handing a bounded generic a deeply-mutable type is what the rule has to catch, and blaming the declaration would name a def that is correct for every other instantiation. An unbounded generic parameter is out of scope, and soundly so: with no bound the body has no method, no field read and no == on that value, and no part of the caller's state is observable through it.
  3. Deeply-immutable result. The return type must be transitively free of anything mutable, with no resource, no live BytesBuilder or BytesReader and no Future, and no mutable alias to internal state escapes (H0608). Finalized bytes, Arc-shared and immutable, qualifies; a builder does not.

With all three, the function's only observable behavior is return = f(inputs). It is referentially transparent, a pure context may call it, and the optimizer and comptime evaluator may treat it as any pure def, the usual non-termination caveat aside. It is the lightweight checked subset of uniqueness and region types, Hanki's runST without the rank-2 machinery.

@encapsulated
def join_bytes(a: bytes, b: bytes) -> bytes
  buf = BytesBuilder.new!()   # rule 2: the builder is allocated *here*
  buf.extend!(a)              # rule 1: extend! is an empty-effect-row action
  buf.extend!(b)
  buf.finish!()               # rule 3: only the immutable bytes escapes
end

join_bytes has no ! and is callable from meta, where-invariants and other pure code. The full design, the immutability lattice, the optimizer-soundness argument and the reason serialization needs no Encode or @derive change, is in docs/design/encapsulated.md.

Non-substitutability in the row: local and runtime_state

A function type states only its effect row, and an action with an empty row would leave a closure's inferred row empty. Such a closure is type-identical to a pure closure: storable in a (u8) -> () field, and invocable from a pure def, a pure combinator like fold, a bare-dot prop read, or the comptime evaluator. Two row atoms close that, and both are enforced. Pure-def substitutability is a checked property at every boundary:

effect local and effect runtime_state declarations are rejected as reserved names, like state. The three atoms differ in where they may then be written: state nowhere, local only on a function type, runtime_state in any effect row, which is how a caller of the log knob declares it.

Debugging & observability

The stance is observe, do not interrupt, and every diagnostic tool writes to stderr, the developer channel outside the effect-tracked contract with the world. Three tools cover it: inline printing with dbg! (the one effect exemption, below), and live actor observation with sys.actors! and sys.get_state!, following the BEAM model of observing without stopping.

For a bug you capture and study afterwards, the complement is deterministic replay. hanki run --deterministic, and hanki test --deterministic, serializes the actor threads through a seeded scheduling gate, and the interleaving, and therefore the program's output bytes, is a pure function of (program, inputs, seed). --seed N picks a different interleaving and implies --deterministic; the bare flag runs the canonical seed-0 schedule. The gate yields at every actor park point (mailbox wait, blocking send, await, actor.await_timeout!, spawn, time.sleep!) and at every sys.* OS-seam crossing, and seeds therefore steer the order of observable effects and not only of message dispatches.

Time is virtual under the gate. time.sleep! parks the actor on a deterministic clock that advances to the earliest sleeper's deadline only when no actor can run: a deterministic run sleeps in zero real time, and actors that are merely sleeping never count toward a deadlock. actor.await_timeout! deadlines sit on the same clock, and a timed-out await also costs no real time and can never be misreported as deadlocked. Both apply while the program only ever waits on itself. A deadline that comes due against an actor parked in a real OS call is spent in real time, for the reason the scoping notes below give. Clock reads, time.now_ms! and time.monotonic_ms!, draw from the same virtual clock, and even a program that prints timestamps replays byte for byte under a fixed seed.

Two things follow. A flaky interleaving bug reproduces by replaying its seed. And a schedule on which every live actor is blocked is detected as a deterministic deadlock, reported to stderr in place of hanging: hanki run exits 251, and a deadlocking test records one failure while the suite continues.

Three scoping notes. External nondeterminism (subprocess output, network peers, stdin) is an input and no interleaving, and "same bytes" applies only where inputs are fixed. Second, an actor blocked inside a slow OS call (a stdin read, a socket, a subprocess) retains its turn and pauses every other actor until the call returns, and the earliest deadline another actor is waiting on bounds that call in real time, a virtual clock being unable to reach a deadline while a real call has the turn. The gate spends the deadline on the pending call in place of jumping over it: a peer that answers within the bound wins, and one that never answers hands the turn back for the deadline to fire. With no deadline pending the call blocks and the whole run waits with it, the turn still being held. No other actor can arm a deadline meanwhile, and a call that starts unbounded remains unbounded. An actor parked in one never counts toward the all-blocked determination, and a reported deadlock still means what it says. Third, two actors that rendezvous through the OS, one actor's net server read blocking on another actor's write, can self-deadlock under the serialized schedule; the gate understands mailbox-level waits alone.

Two operations are refused outright and are never treated as an input: process.run_attached! and process.run_attached_opts! (§17), which hand the terminal to a child. A captured subprocess's output is an input like any other, a child that owns the tty is an interactive session, and no seed replays what a user types into one. The gate faults the call, exit 1 with the same reason text on both tiers, in place of producing a run that claims a reproducibility it cannot have. They are the only sys.* seams that decline under the gate: laying an environment on an attached child changes what it inherits and not who owns the terminal, and the options form declines for the reason the bare one does.

Both tiers run it. hanki run and hanki test take --deterministic and --seed, and an AOT-compiled binary reads the same through HANKI_DETERMINISTIC=1 and HANKI_SEED=N in the environment, leaving a compiled program's main(args) argv untouched. The gate, the park points (mailbox wait, send, await, spawn, time.sleep!, and every sys.* OS-seam crossing), the virtual clock and the seeded random stream are the tier-agnostic rtcore core, and a given seed replays byte-identically on both tiers: an AOT binary and hanki run produce the same interleaving for one seed.

There is no stop-the-world step debugger. Hanki's bug classes are logic, caught up front by types, effects and dbg!, and concurrency and lifecycle, which need observation and no stepping. Stepping distorts the actor timing the bug depends on, and stop-the-world fits a share-nothing actor language poorly. Live-attach tooling beyond those two readouts, tracing, a remote shell and state-replace, is staged by cost and extends the observe model.

Debug-trace exemption: dbg!

dbg!(expr) is the one compiler-blessed exemption from effect propagation. It evaluates expr, prints [file:line] <source> = <value> to stderr, and returns the value unchanged. It is drop-in around any subexpression (let y = dbg!(f(x)) + 1) and may be called from a pure function without forcing [io] onto its callers:

struct Point
  x: i32
  y: i32
end

def slope(p: Point) -> Option<i32>   # pure — no effect row
  dbg!(p)                            # stderr: [main.hk:7] p = Point(x=3, y=4)
  p.y.checked_div(p.x)               # a runtime divisor goes through checked_div (§3)
end

Effects track a program's semantic contract with the world: stdout, net, fs, throws. dbg! writes to a developer diagnostic channel outside that contract. Purity tracking and debug observation are orthogonal, and every effect-disciplined language arrives at the same exemption (Haskell Debug.Trace, Koka trace, Rust dbg!). The ! spelling marks it as an action, no one mistakes it for pure logic, and it flags itself for removal.

It renders any value structurally, structs with their field names, sum variants, lists and primitives, with no Display impl required. The names come from the argument's static type, which the runtime value representation erases.

dbg! works on both tiers, and the rendering is identical, the AOT runtime sharing the bytecode tier's structural renderer. hanki check, the REPL, and ordinary unconstrained hanki run, test and fuzz accept it. A restricted execution, any of those three commands with --allow or --deny, instead fails before execution when a selected entry or test can reach dbg!; pass the explicit --allow-dbg escape hatch to retain diagnostic output. hanki build is the shipped-code boundary and always applies the same fail-closed check before it creates out/ or invokes the native backend, with hanki build --allow-dbg as its explicit opt-in. The audit follows the lowered call graph: a pure helper counts, a spawned actor contributes all of its handlers, and dead code does not; function values conservatively over-approximate. hanki effects PATH --dbg exposes the exact audit as text, or as a hanki-effects-dbg-v1 JSON envelope {schema, entry, sites: [{symbol, path, line, column}], loads_modules} under --format=json. Runtime-loaded source cannot be enumerated statically. The loads_modules field flags the caveat, and each module.load! / reload! checks the loaded exports at that boundary. A restricted bytecode host passes its --allow-dbg choice through; an AOT host bakes the build choice into its load baseline. A denied load is a catchable ModuleLoadError. Loading therefore cannot launder a diagnostic write.

When enabled, an un-monomorphised generic parameter still renders structurally: the compiler threads each rendered type parameter's concrete layout from the call site as a hidden shape witness, and dbg!(x: T), or a nested dbg!(xs: List<T>), prints field and variant names on both tiers even though the bytecode tier lowers one generic body. Two positional fallbacks are narrow: a type parameter that never appears as a direct value parameter (m: Map<K, V> with no k: K or v: V), and a generic function used as a value (f = show!, called indirectly).

Actor introspection: sys.actors!

sys.actors!() prints a one-line-per-actor table of the live actor system to stderr, giving each registered actor's id, class where known, liveness, mailbox depth and capacity, and supervisor, then returns ():

def main!() -> () [io]
  sys.actors!()
end

Output on stderr:

actors (1):
  #0.0 <none> alive mailbox 0/1024 supervisor <root>

An id prints as slot and generation, #1.0, both halves of the ActorRef (§15, Actor identity and slot reuse): a slot is recycled with a bumped generation, and the slot number alone names its current occupant and not the actor a row refers to. A supervisor whose id is not among the rows is marked <gone>.

Unlike dbg!, it is not effect-exempt. It is an ordinary [io] action: it observes runtime structure and writes a diagnostic, it takes [io] like any other output, and it cannot be called from pure code. It works on both tiers, bytecode and AOT, each labelling a spawned actor with its class name; the bare program actor, the root, has no class and shows <none>. It is structural only and never reads an actor's state. Live state inspection is sys.get_state!, below.

Live actor state: sys.get_state!

sys.get_state!(handle) prints the current state of one running actor, addressed by its ActorRef<T> handle, to stderr, with its state fields rendered as a struct, the field names recovered from the actor's static type and the values rendered as dbg! would render them, then returns (). It is the live counterpart to the crash-time state dump below: the same renderer, triggered on demand against a running actor.

actor Counter
  state n: i32 = 0

  on increment() -> ()
    n += 1
  end
end

def main!() -> () [io, throws actor.SendFailed]
  c = spawn Counter
  c.increment()
  sys.get_state!(c)   # stderr: actor #1.0 (Counter): state: Counter(n=1)
end

The snapshot is taken at the actor's next inter-handler safe point, a priority request the actor services ahead of its pending mailbox messages, in the gap between handler runs. State is never reached for from another thread. Hanki actor state is share-nothing and this preserves that, following the BEAM model of observing without stopping. Outcomes other than a clean snapshot are reported on stderr and never by blocking:

Like sys.actors!, it is an ordinary [io] action and no dbg!-style exemption, and it works on both tiers. It is spelled get_state! and never state!, after Erlang's sys:get_state. state is an ordinary identifier (§2), and the verb is what marks this as an observation in place of a field read.

Divergence: crash!

crash!(msg: string) -> Never is the divergence primitive: it never returns. Use it on a branch you have proven unreachable, the "this cannot happen" assertion the type system cannot express:

type Color
  Red
  Green
  Blue
end

def render!(c: Color) -> string [Crash]   # an action — a pure `def` cannot crash
  match c
    Red   -> "red"
    Green -> "green"
    _     -> crash!("Color had an impossible variant")
  end
end

Its result type is Never (§4), which coerces to any expected type, and a crash!(...) fits any arm without a placeholder. It takes the Crash effect, its own uncatchable effect atom, written in the effect row as in [io, Crash], and a pure def with an empty effect row cannot call it: pure functions are total and never crash. Crash takes no type parameter, unlike throws E, since it cannot be caught. catch e: Crash is a compile error.

Crash is not a capability, and the restricted-execution gate treats it as it treats runtime_state: a policy has nothing to grant or withhold about a divergence marker. --allow Crash and --deny Crash are refused as an unknown capability, and a Crash in a program's row never denies it under an allow-list: --allow io runs a program that can crash!. hanki effects still lists it, the report being the wider view, and "can this program diverge" is a question worth asking.

When reached, crash! terminates like any other runtime fault (§15) and not as a throw. Inside an actor it kills that actor and fires its supervisor's on actor_died; at the program root it exits 252 printing crash: <msg>; under hanki test it fails the current test. It is a production construct, valid on both tiers, bytecode and AOT.

Typed holes: ???

??? is a typed hole, a placeholder for code you have not written yet. It type-checks anywhere an expression is expected. Its type is Never (§4), and like crash! it coerces into any position. Unlike crash! it is effect-free: a hole charges no effect, Crash included, and it is legal in a pure def as readily as in an action. Sketch a program's outline and leave the gaps as holes:

def parse_user!(line: string) -> Result<User, FormError> [io]
  fields = ???              # what goes here?
  ???
end

hanki check type-checks the surrounding program and reports, for every hole, the type the context expects there and the effect budget, the effects permitted at that point:

parse_user.hk:2:12: hole[H0250]: this hole expects `List<string>`; effect budget here: [io]
parse_user.hk:3:3: hole[H0250]: this hole expects `Result<User, FormError>`; effect budget here: [io]

This drives spec-first development: write the types, let the compiler dictate each gap, fill it to fit. hanki check, the LSP and the REPL leave holes non-blocking. check exits 0 and reports every hole as advice, severity hole on the --format=json envelope; the REPL does the same for each submitted block. A hole has no runtime value. A permitted execution that reaches one diverges like crash!: it prints crash: hole reached and exits 252 on both tiers.

Executable boundaries fail closed by presence in the selected root's checked module closure, imports and dependencies included, without a call-graph guess. hanki run, hanki test and hanki fuzz reject every such hole before a rift is prepared or any program effect runs. --allow-holes is their explicit development escape: every site remains reported, and reaching one exits 252. Executable doctests follow test; an illustrative hole belongs in a hanki skip fence. A runtime module.load! or module.reload! applies the same rule before binding, spawning or swapping code, and a failed reload leaves the old module live. A host started by run, test or fuzz with --allow-holes passes that development allowance into its loads; an ordinary host rejects the load with all sites in its ModuleLoadError.

hanki build also rejects holes by default before creating out/, building rifts, lowering or linking. AOT development remains possible through hanki build --allow-holes; its artifacts are quarantined under out/holey/ and never overwrite the canonical executable, object or shared-library path. Each contains a durable .hanki_holes section with the sites, and LLVM-IR output contains equivalent !hanki.holes named metadata. Copying or renaming the artifact cannot erase its identity. Such an AOT host inherits the permissive load rule above. Ordinary AOT artifacts are always closed. This uses the same AOT tier and hole lowering. The quarantine excludes an explicit sketching build from ordinary packaging and deployment paths.