Research and reference implementation for a general-purpose, verification-native programming language built on Machine-Native Complexity Standard (MNCS) principles.
Project status: semantic-model and source-representation research with executable prototypes. No final grammar, compiler stability, or production suitability is claimed yet.
Conventional languages primarily describe operations, data, and control flow. Verification tools then reconstruct behavioral relationships after the program has been written. This project investigates the opposite arrangement: contracts, effects, capabilities, assumptions, failure semantics, resource bounds, and evidence are part of the program's meaning from the beginning.
The intended language is machine-native without being machine-exclusive. Humans, agents, compilers, auditors, and independent verifiers should be able to inspect the same semantic structure.
An MNCS-oriented program should make it possible to answer:
- What does this component claim?
- What state may it observe or modify?
- What authority does it possess?
- What assumptions does it depend upon?
- What evidence supports each property?
- Where does proof stop and trust begin?
- What must be re-verified when the component changes?
- How can the system diagnose and improve itself without laundering evidence or silently broadening authority?
docs/— vision, architecture, syntax research, recursive refinement, terminology, trust model, and explicit non-goals.spec/— early normative semantic and representation documents.rfcs/— design proposals that can evolve independently of the specification.crates/mncs-model/— an executable Rust model of the initial semantic objects and validation rules.crates/mncs-syntax/— deterministic, tokenizer-neutral source representation metrics.crates/mncs-cli/— validation and syntax-tournament commands.examples/— semantic manifests, competing source candidates, canonical semantic forms, and semantic patches.
The JSON manifests and source candidates are experimental transport and research representations. They are not yet a selected production grammar.
The 0.1 model contains:
- modules and functions;
- typed inputs and outputs;
- contract clauses;
- declared effects;
- required capabilities;
- explicit assumptions;
- evidence claims and verifier identities;
- failure modes;
- machine-readable validation diagnostics.
A key initial rule is that every effect must identify an authorizing capability, and that capability must be declared by the function. Evidence must reference a declared contract property rather than floating as unbound metadata.
cargo run -p mncs-cli -- validate examples/account-transfer.mncs.jsonThe command emits a JSON validation report. The valid example should exit successfully.
The following example intentionally performs a network effect without declaring the required capability and should be rejected:
cargo run -p mncs-cli -- validate examples/invalid-undeclared-effect.mncs.jsonThe current hypothesis uses three related representations:
Zig-influenced human source
↕ deterministic semantic round trip
compact canonical semantic form
↓
high-level MNCS IR and verified SSA
Recursive tooling also exchanges semantic patches that target stable graph identities rather than unrestricted source-text replacement.
Run the account-transfer tournament:
cargo run -p mncs-cli -- syntax-tournament \
examples/syntax/account-transfer.tournament.jsonThe tournament compares three human-source candidates and one canonical machine form against the same 23 declared semantic claims. It reports deterministic lexical units and non-whitespace characters per claim. These are tokenizer-neutral comparison metrics, not exact token counts for a particular model.
See Source Syntax Laboratory, Source Representations, and RFC 0005.
The current direction is:
human source syntax (experimental candidates)
↕
canonical semantic graph/form
↓
high-level MNCS IR
↓
verified SSA IR
↓
LLVM IR / Cranelift IR / another backend
↓
machine code + evidence manifest
The important design boundary is between the verification-native semantic layers and a conventional optimization backend. Backend claims such as non-aliasing, no-overflow, or in-bounds access should ideally be emitted only when established by evidence rather than inserted optimistically.
Recursive refinement is a foundational language requirement, not only an orchestration feature supplied by the Forge or RAVEL. The language should expose its semantic graph, evidence graph, diagnostics, causal slices, and transformation history in forms that can be consumed by later verification and repair cycles.
The intended loop is bounded and evidence-driven:
observe semantic and evidence state
↓
localize a failed or weak obligation
↓
propose a repair in an isolated candidate state
↓
declare intended improvements and protected properties
↓
run independent targeted verifiers
↓
compare semantic, authority, complexity, and evidence deltas
↓
promote or reject under explicit policy
↺
A generator must not silently modify the trusted baseline or certify its own repair merely by repeating the cycle. Recursion depth, authority, mutation scope, candidate count, verifier calls, and resource use must be bounded. See Recursive Debugging and Refinement and RFC 0004.
- MNCS defines the broader standard, contracts, complexity concepts, and verification philosophy.
- MNCDS explores deterministic and structural representation where applicable.
- MNCS Language investigates how those relationships can be expressed directly in a general-purpose language, including semantic structures for recursive introspection and repair.
- MNCS Forge can analyze, verify, localize failures, test candidate transformations, and produce evidence for MNCS-language components and conventional code.
- RAVEL can coordinate recursive, distributed, multi-agent, and multi-verifier refinement across machines and trust boundaries.
MNCS must remain applicable to existing languages even if this project never becomes production-ready. The standard therefore does not depend on this language project.
- Semantics before syntax. Surface choices must preserve the semantic model rather than define it accidentally.
- Explicit authority. Ambient filesystem, network, process, clock, randomness, and credential access should not be assumed.
- Closed effects. Undeclared effects should be rejected or isolated at a visible trust boundary.
- Named assumptions. Verification results must state the assumptions on which they depend.
- Evidence is addressable. Every claim should identify its property, verifier, status, and optional artifact.
- Proof gradients are honest. Tested, analyzed, verified, and externally verified are different states.
- Unsafe behavior is bounded. Low-level operations may exist, but their boundary and obligations must be explicit.
- Incremental verification. A change should invalidate the smallest defensible evidence subgraph.
- Human inspectability. Machine-native structure must remain understandable without an LLM.
- Backend conservatism. Optimization promises should be generated from established facts.
- Recursive refinement is bounded and reviewable. Promotion requires explicit policy, protected-property checks, and sufficient independent evidence.
- Semantic density beats character density. Representation efficiency is measured against complete, equivalent claims rather than raw brevity.
- Role-specific representations are allowed. Human source, canonical agent form, semantic patches, and verified IR need not use the same notation.
The immediate target is Milestone 0.1 — Executable Semantic Model, with the source syntax laboratory operating as a cross-cutting research track. See ROADMAP.md.
The project is early enough that a precise counterexample is often more valuable than a large implementation. Read CONTRIBUTING.md, then use an RFC for changes that alter the semantic model or source representation requirements.
Apache License 2.0. See LICENSE.