Language Features

Language Features

Mined from the actual implementation (crates/compiler/src/), not the design docs — see LANGUAGE.md for the authoritative reference and Architecture for where each check below actually runs in the pipeline.

A feature existing in the type system isn't the same claim as it running today. The interpreter was removed entirely (2026-09) — a construct native codegen doesn't reach yet is a compile-time rejection, not something that still runs interpreted. Sections below are marked [compiled] or [not currently running] accordingly; see Honest Scope & Roadmap for the full, currently-accurate list and PUBLIC_ROADMAP.md for what's landed most recently — this is the one page on this wiki most likely to drift out of sync with a fast-moving compiler, so treat the roadmap doc as the tiebreaker.

Types

Signed/unsigned ints (i8..i64, u8..usize), f64 (IEEE-754, saturating), bool, unit, str (UTF-8, Arc<str>-backed), box T (single-owner heap), &T (read-only borrow of an identifier), thread T, chan T (unbounded MPMC), sandbox, tcp/tcp_listener, file, VerifiedIdentity/RoleView/ClaimView (identity proofs), Vector(T, N) and Matrix(T, R, C) (fixed-shape, fixed-length — Vector(f64,3) ≠ Vector(f64,4)).

Ownership & affine types

box T is single-owner; moving into spawn/send/stop consumes it. &T is a read-only borrow. The ownership checker (ownership.rs) enforces the linear discipline statically — no use-after-free, no aliased mutation, no GC. Cyclic structures are the known hard case (an arena escape hatch is the planned answer).

Concurrency

• [compiled] spawn f(args) — a real OS thread, returns thread T; join consumes it once. Backed by a real, compiled, admission- controlled runtime kernel (crates/runtime-kernels/), not the interpreter's own thread bookkeeping.
• [compiled] chan T — unbounded MPMC channel; the handle is freely copyable, the payload moves through send.
• [not currently running in any form] sandbox worker(args) — a real, separate OS process (a fresh nirdosha invocation), affine sandbox handle; stop terminates it. A handle that goes out of scope unstopped still kills its process (no zombies) — deterministic cleanup, not discipline-dependent, when this was interpreter-backed; native codegen doesn't reach it yet.

There is no mutex in the language, so a lock-ordering deadlock is not expressible at all. Hot paths that want shared-memory locks get re-cast as messages — but messages have their own deadlock shape (a recv nobody ever sends to, two threads mutually joining each other), and that one is expressible. The compiled runtime kernel (crates/runtime-kernels/ src/kernel/) catches it dynamically and aborts, not left to hang: a join-cycle is detected precisely (a real wait-for graph over join edges); a recv gets a coarser, still-sound fallback (every live thread simultaneously blocked — the same condition Go's own runtime deadlock detector checks, generalized to also catch a join-cycle mid-program, which Go's whole-process-only check misses). The one disclosed gap: a recv blocked forever while some other, unrelated thread stays busy on its own work is invisible to the coarse check — that would need real points-to tracking of channel handles, not attempted.

Effects

effect(...) annotations are fully inferred by default (no notation paid unless load-bearing). A declared annotation is checked against what the body actually does — an effect performed but not declared is a compile error, not a silent gap. effect(pure), effect(io), etc.

Refinement types & SMT

Integer/buffer bounds proofs are discharged by an SMT solver (Z3, via refine.rs/smt.rs) at compile time, tiered: Tier-1 attempts a static proof; Tier-2 inserts a runtime guard when a fact isn't SMT-decidable in scope; audited "justification" { ... } is the one documented escape hatch that suppresses guards with a human-language justification — the one place a human review gate stays mandatory even in an otherwise unsupervised pipeline.

Determinism

rand_seed(seed) resets a from-scratch SplitMix64 RNG (no OS entropy, no hidden global state). rand_f64/rand_gaussian draw from it. A simulation's random draws are byte-for-byte reproducible from a seed — the foundation of crates/bench/'s run-deterministic (run + hash-check) and of auditable simulations. This is also the concrete, shipped slice of the project's aspirational "tamper-evidence" requirement — see Design Philosophy row 10.

Identity, roles, claims

oidc_validate_token(...) validates an externally-issued OIDC/JWT ID token (HMAC-SHA256) and returns a VerifiedIdentity — the runtime never mints tokens, only consumes them. check_role/extract_claim (and their dotted-path siblings for nested IdP schemas like Keycloak) produce RoleView/ClaimView proofs. requires(role: "admin")/requires(claim: "department", "cardiology") on a fn demands such a proof at the call site — capability-gated, statically tracked.

Workflows

workflow Name { data { ... } state ... } declares a durable, named state machine — states, on <Event> -> <Target> transitions (a link mark makes one an unauthenticated, single-use magic link), and on_entry/on_exit actions that can call the notification builtins (send_email/send_sms/send_push/notify). It's pure desugaring, not a new runtime primitive: workflow_lower.rs turns the block into ordinary fn/enum/struct declarations right after parsing, so every later pass never sees workflow syntax itself. on_entry/on_exit actions are designed to be crash-durable (logged before running, replayed on restart), the same discipline transact uses. A state can also declare owner: role(...)/claim(...) (who may fire its outgoing events, checked per-instance at runtime, not statically) and label: "...", for a generated "Workflows" nav section in a live UI.

Status is moving fast here — check PUBLIC_ROADMAP.md for the current, exact answer rather than trusting this paragraph. As of the interpreter's removal, workflow (like transact/db/mq) had no compiled path at all — nirdosha build/emit-llvm cleanly rejects a program using it, naming the specific unsupported builtin, never a silent mis-compile — and native codegen support has been actively landing since. nirdosha emit-ui renders the derived "Workflows" nav section into a static page either way (no server, no live transitions) — see The UI Engine. Full grammar and protocol in WORKFLOW.md.

Data types & generics

struct, enum, and match (exhaustive, no wildcard/binding patterns in v1). Type parameters are concrete-per-instantiation: Pair(i64, str) and Pair(f64, bool) are different, unrelated types — no monomorphizer pass exists or is needed. Option(T) and Result(T, E) are ordinary generic enums injected into every program at parse time. Affinity propagates through struct/enum fields and through a generic instantiation's own concrete type arguments, the same way it does through box.

Dense linear algebra

Vector and Matrix with transpose, dot, cross (3-vectors), zeros/ones/identity, sum, len, norm/norm1/norm_inf, frobenius_norm, trace, matrix×matrix and matrix×vector multiply with shape checking at typecheck time. Vector * Vector is a type error by design (ambiguous inner vs. outer product) — use dot(). The whole linalg feature set is modeled on Julia and is now compiled (see Benchmarks).

I/O & networking

[compiled] print, file handles (open/read/write/stop), tcp client (connect), tcp_listener (listen/accept/stop).

[not currently running in any form] JSON, a db builtin (SQLite via rusqlite, or Postgres via postgres/postgres-native-tls — picked by db_connect's own connection-string scheme, see PROTOLANG_PORT.md's "Locked design 5: DB"), transact semantics (see TRANSACT.md) including cross-process transactions, and a redis-backed message queue — all fully designed and documented, all previously interpreter-backed and verified working in that form, none reachable from nirdosha build/ emit-llvm right now. nirdosha build/emit-llvm name the specific unsupported builtin and reject the program rather than mis-compiling it; see Honest Scope & Roadmap and PUBLIC_ROADMAP.md for what's landed in native codegen since.

Structured diagnostics

Every error — type, ownership, runtime — is a real, structured Diagnostic value internally (lib.rs::Diagnostic), not a bare string assembled on the spot — a type/ownership error carries the specific TypeErrorKind/ OwnershipErrorKind variant, span, and (where relevant) names of the construct involved. Today's CLI prints these as formatted plain text (nirdosha build/emit-llvm's own eprintln! output), not JSON on stdout behind a flag — an agent-facing JSON diagnostic mode is a real, disclosed gap between what the internal type already supports and what the CLI currently exposes, not a shipped feature yet. nirdosha emit-ast does emit real JSON today, just for the parsed AST of a program that typechecks or not, not for the diagnostics themselves. See LLM Integration for the full, current mechanism this enables and doesn't yet.