Design Philosophy

Design Philosophy

Source: goal.md, the project's research brief.

The constraint that shapes everything

Before any feature decision, one theorem sets the ceiling: Rice's theorem (1953). For any non-trivial semantic property of a program — does it terminate, does it race, does it overflow — no algorithm can decide that property correctly for every program in a Turing-complete language. Not "nobody has found a good enough algorithm yet." Provably never, for any algorithm, ever.

This doesn't kill the project; it dictates its shape. Every language that has actually shipped compile-time guarantees for properties like these — Rust, SPARK Ada, F*, Pony — routes around Rice's theorem the same way: the type system is deliberately conservative. It accepts a smaller language than "everything a human (or model) could write correctly," in exchange for being able to say, with certainty, "everything this accepts is safe." Programs that are actually correct but that the checker can't prove correct get rejected. That isn't a flaw — it's the price of the guarantee. Any pitch that promises "catches every bug, rejects nothing valid" is promising something that doesn't exist.

So the real design question isn't "how do I catch everything." It's where the conservative boundary sits, and what the programmer — human or model — does at it. That question matters equally for formal-methods correctness and for whether an LLM can reliably work around the boundary when it hits it.

Twelve requirements, treated as one set

Roughly half of Nirdosha's requirements are things a compiler can prove (hard); half are things that can only be measured against how humans and models actually behave (soft). The project's core thesis is that neither half is optional relative to the other:

• A design that satisfies only the provable half is Idris2 or ATS — correct and nearly unused.
• A design that satisfies only the measured half is Go or Python — usable and unsafe.

Both halves have to be designed together from the start, in one language, not as a safety core with usability bolted on afterward.

#	Requirement	Class	Mechanism	Prior art it's grounded in	The catch
1	No GC, no manual free()	Hard — proof	Ownership / linear types + region inference	Rust, Austral, ATS	Cyclic structures fight the discipline — needs an arena escape hatch
2	No data races	Hard — proof	Type system rules out simultaneous mutable aliasing, statically	Rust (borrow checker + Send/Sync), Pony (reference capabilities)	Only covers what the type system can see — FFI/unsafe boundaries reopen the hole
3	No deadlocks	Hard — proof by construction (lock-ordering) + runtime detection (recv/join)	No mutex primitive exists in the language at all; concurrency is async messages	Pony — no mutex exists, so a lock-ordering deadlock isn't expressible	Messages have their own deadlock shape (a recv nobody sends to); that one is caught at runtime, not statically prevented
4	No int / buffer overflow	Hard — SMT-discharged, tiered	Refinement types on integers/indices, discharged by an SMT solver	SPARK Ada (avionics, rail, defense since the 1990s), F*/Low* (HACL* ships in Firefox, Linux WireGuard), Dafny	Not every arithmetic fact is SMT-decidable — needs a defined fallback, not silent failure
5	Native, hardware-speed codegen	Hard — engineering	AOT via LLVM/clang, no interpreter, no GC pauses	Rust, ATS, Low* (→C), SPARK	A bespoke ISA would be R&D that swallows the project — LLVM already captures that instinct
6	No steep learning curve	Soft — measured	Small, orthogonal grammar; one idiomatic way to do a thing; safety machinery silent by default	Go, Python — optimized for onboarding over expressiveness	Directly in tension with 1–4: ownership, effects, refinement types are exactly the extra notation that raises the curve
7	Easy for an LLM to write/reason about	Soft — measured, one hard sub-property	Unambiguous (LL(1)) grammar — a decidable, checkable property; keyword-heavy over symbol-heavy syntax; structured, not prose, diagnostics	Grammar-constrained decoding research (outlines, guidance, LALR-constrained sampling) shows markedly higher reliability under a formal grammar	Real-world LLM code quality is dominated by training-corpus volume — no grammar design fixes a brand-new language starting at zero corpus. Mitigated by shipping the grammar/decoder spec with the language itself (see LLM Integration)
8	Logical, composable syntax	Proof (compositionality)	Complex operations visibly compose from a small set of fundamentals	—	—
9	AI as a first-class citizen	Measured; agent-facing API is hard-typed	Structured diagnostics, fragment validation, deterministic execution	—	—
10	Tamper-evidence — detect "alien" code in a binary	Proof (reproducible builds, content-addressed source)	Aspirational — not built	—	The honest foundation today is rand_seed's deterministic RNG (byte-for-byte reproducible runs), which a future implementation would extend, not the full claim itself
11	Closed product types, sum types, generics	Proof (decidable)	struct/enum/match + per-instantiation generics	—	Narrowly scoped on purpose: no traits, no HKTs, no subtyping — so it doesn't become its own research project
12	Capability-gated access	Proof (statically checked at the call site)	requires(role/claim: ...) + acquired RoleView/ClaimView proofs	—	Runtime role-mapping (app role ↔ IdP role) is still a real lookup, not compile-time-erased

Row 11 wasn't in the original ten — it was added after a real porting exercise (PROTOLANG_PORT.md) produced three "Blocked" and four "Rejected" verdicts that all traced back to one missing layer: no product types, sum types, or generics. That's the project's own discipline in practice — a gap discovered by actually trying to port real programs, not by introspection, and folded back into the requirement set rather than left as a known limitation.

Why this matters if you're an LLM

Every other requirement in this table is downstream of one fact: you will be writing this code with no human reviewing every line before it runs. That reframes what "safe" means. A language that is safe if used correctly is not safe for an unsupervised agent — it's safe for a careful human who can be trusted to notice when they're at the edge of the conservative boundary. Nirdosha's bet is that the boundary itself has to be something your sampler can be mechanically constrained to (row 7's hard sub-property, LL(1) → GBNF), and that hitting the boundary has to produce a structured proof obligation you can act on programmatically, not a paragraph of English you have to interpret. See LLM Integration for exactly how that's implemented, and Architecture for where each of these checks actually lives in the compiler.

Further reading

• goal.md — the full research brief this page summarizes, including the per-phase implementation plan.
• Nirdosha_Unified_Plan.md — how the twelve requirements map onto actual build phases.
• nirdosha_row11_amendment.md — the product/sum-type/generics amendment in full.