DEV Community

Arun Soman
Arun Soman

Posted on

Nirdosha: a language that treats correctness, durability, and identity as compiler problems

Every language promises safety. Nirdosha's example suite reads like an audit of that promise — each file exists to demonstrate one guarantee, with the rejected programs living in the test suite.

  • Ownership without a garbage-collector personality. box moves on assignment; a second use is a compile-time error. & borrows read without taking. The same affine discipline applies to every resource handle — files, sockets, database connections, message queues, sandboxes — so "forgot to close it" is a type error too.
nir
`fn consume(b: box i64) -> i64 {
    return *b
}

fn main() {
    let a: box i64 = box 10
    print(consume(a)) // moves `a`; using it again would not typecheck
}`
Enter fullscreen mode Exit fullscreen mode
  • Effects you don't annotate until you want to. Effects are inferred by default; if you declare effect(pure) and the body does I/O, that's a compile error, not a linter warning.

  • Concurrency that can't alias. spawn's arguments move exactly like a normal call's, so two concurrent computations can never hold the same affine value. Channels are multi-producer, multi-consumer; sending a box moves it across the wire. The same chan/send/recv syntax works across an OS-process boundary via sandbox — the transport changes, the source doesn't.

  • Transactions as a language construct. transact generates an idempotency key before anything runs, records intent durably, verifies before committing, compensates on failure, and leaves non-terminal entries for replay after a crash. If the retry budget runs out, it traps rather than guessing.

  • Identity in the type system. Nirdosha is an OIDC relying party: it validates JWTs against JWKS and never mints identity tokens. A requires(role: "physician") function's value is unobtainable without proof — acquire is the only path, and calling it directly is a compile-time error.

  • Math for the mission. Dense linear algebra, a linear Kalman filter, and WGS84 geodesy are builtins. The benchmark suite isn't "solve one huge system" — it's 200,000 predict/update steps of a constant-velocity tracker, because that's the actual workload shape.

  • Apps, not toys. nirdosha serve runs real applications from the examples folder: an online store (SQLite-backed CRUD, checkout against a mock payment gateway, order events on a message queue), a revenue-assurance tool (reconciliation as a single SQL statement, dashboards derived by naming convention), and an enterprise trade-finance platform with maker-checker approval governance. The web UIs are derived from structs via emit-ui — not hand-written.

  • The examples are candid about what the language can't do yet — no string concatenation, affine handles without borrowing, fixed entity counts in actor simulations. That honesty is the point: every limitation is documented in the file that demonstrates the feature.
    try it out

Top comments (0)