Language Features

Language Features

Mined from the actual implementation (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.

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

• spawn f(args) — real OS thread, returns thread T; join consumes it once.
• chan T — unbounded MPMC channel; the handle is freely copyable, the payload moves through send.
• 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.

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. interpreter::DeadlockRegistry catches it at runtime instead: 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 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 nirdosha serve's automatic POST /api/<fn> RPC exposure — and every other later pass — never sees workflow syntax itself. on_entry/ on_exit actions are crash-durable (logged before running, replayed on restart), the same discipline transact already uses. Interpreter-only, the same way transact/db/mq are (see Honest Scope & Roadmap): nirdosha build/ emit-llvm cleanly rejects a program using workflow, naming the specific unsupported builtin, never a silent mis-compile. A state can also declare owner: role(...)/claim(...) (who may fire its outgoing events, checked per-instance at runtime, not statically) and label: "..." — nirdosha serve/emit-ui render a generated "Workflows" nav section from these. Full grammar and runtime 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

print, file handles (open/read/write/stop), tcp client (connect), tcp_listener (listen/accept/stop), 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.

Structured diagnostics

Every error — type, ownership, runtime — has one structured shape (Diagnostic JSON via --format=json), not English prose. This is what makes the LLM self-repair loop possible: the model gets a machine-parseable proof obligation back, not a sentence to guess at. See LLM Integration for the full mechanism this enables.