| Component | Language | Purpose |
|---|---|---|
oo7-core |
Rust | Parser, AST, typechecker (L1-L9), evaluator, semantic analyser, 7 codegen backends, proof dispatch |
oo7-cli |
Rust | CLI frontend — REPL, file execution, format, compile |
oo7-lsp |
Rust | Language Server Protocol — diagnostics, hover, completion, goto-def, references |
linker |
Rust | 007 IR + native object linker, symbol resolution, relocations |
interpreter |
Rust | Multi-language backend registry, 31 registered backends |
spec/ |
EBNF / AsciiDoc | Language specification, grammar (1127 lines), type system spec |
proofs/idris2/ |
Idris2 | Formal proofs: Harvard invariant, tropical semiring laws, CNO, type soundness, session duality, determinism (6 files, zero believe_me) |
proofs/lean4/ |
Lean4 | Proof obligation templates |
examples/ |
007-lang | Example .007 programs |
docs/ |
Markdown / AsciiDoc | Design journal, papers, audit scorecards |
[.007 source]
│
▼
┌──────────┐ ┌──────────────┐ ┌──────────────┐
│ Parser │────▶│ AST (Harvard│────▶│ Typechecker │
│ (Pest) │ │ separated) │ │ (L1-L9) │
└──────────┘ └──────────────┘ └──────┬───────┘
│ │
│ ┌──────┴───────┐
│ │ Semantic │
│ │ Analyser │
│ └──────┬───────┘
│ │
┌────────────┼─────────────────────┤
│ │ │
┌─────┴─────┐ ┌───┴────┐ ┌─────────────┴──────────────┐
│ Evaluator │ │ Proof │ │ Codegen Backends │
│ (tree- │ │Dispatch│ ├──────────┬──────────┬────────┤
│ walk) │ │(Idris2 │ │ Elixir │ Zig │ QBE │
└─────┬─────┘ │ Lean4) │ │ (BEAM) │ (native) │ (IL) │
│ └────────┘ ├──────────┼──────────┼────────┤
▼ │ WASM │Cranelift │ C │
┌──────────────┐ │ (WAT) │ (.o AOT) │(future)│
│ Trace system │ └──────────┴──────────┴────────┘
│ (decision │ │
│ logging) │ ┌──────┴───────┐
└──────────────┘ │ Linker-mk2 │
│ (007 IR + │
│ native .o) │
└──────────────┘
crates/
├── oo7-core/ # Core library (805 tests)
│ ├── src/
│ │ ├── parser.rs # Pest parser (2071 lines)
│ │ ├── grammar.pest # PEG grammar (742 rules)
│ │ ├── ast.rs # AST — Harvard-separated, 18 DataExpr variants
│ │ ├── typechecker.rs # L1-L9 Kategoria type system (4778 lines)
│ │ ├── eval.rs # Tree-walking evaluator
│ │ ├── semantic_analyser.rs # Discourse-bound semantic analysis (plugin arch)
│ │ ├── formatter.rs # Canonical formatting with comment preservation
│ │ ├── lsp.rs # LSP core: diagnostics, hover, goto-def, references
│ │ ├── effects.rs # Effect system (10 effects including Compute)
│ │ ├── proof_dispatch.rs # Idris2/Lean4 proof obligation dispatch
│ │ ├── metacompiler.rs # EBNF→Pest + grammar validation
│ │ ├── metainterpreter.rs # Meta-circular evaluation (4 modes)
│ │ ├── codegen_elixir.rs # Elixir/OTP codegen (2473 lines, 39 tests)
│ │ ├── codegen_wasm.rs # WASM/WAT codegen (595 lines)
│ │ ├── codegen_native.rs # Zig native codegen (605 lines)
│ │ ├── codegen_qbe.rs # QBE IL codegen (MIT, x86/ARM/RISC-V)
│ │ ├── codegen_cranelift.rs # Cranelift AOT codegen (Apache-2.0, .o files)
│ │ ├── bridge.rs # Pipeline: parse→check→prove→compile→link
│ │ ├── backends.rs # Tier 0: core backends (007, DSL, JSON, shell)
│ │ ├── backends_tier1.rs # Tier 1: BEAM, Idris2, VeriSimDB, LLM, Zig FFI
│ │ ├── backends_tier2.rs # Tier 2: Gleam, ReScript, Nickel, Scheme, WASM
│ │ ├── backends_tier3.rs # Tier 3: HTTP, SQL, Groove, PanLL, Containerfile
│ │ ├── backends_tier4.rs # Tier 4: Lean4, Tropical, Epistemic, Choreography
│ │ ├── backends_tier5.rs # Tier 5: CUDA, Vulkan, Metal, OpenCL, FPGA, TPU, DSP
│ │ ├── dual_ast.rs # Harvard Architecture integrity verification
│ │ ├── source_map.rs # Source position tracking
│ │ └── trace.rs # Decision trace system
│ ├── benches/
│ │ ├── toolchain_bench.rs # Compiler pipeline benchmarks
│ │ └── algebraic_dispatch_bench.rs # Semiring algebra benchmarks
│ └── Cargo.toml
├── oo7-cli/ # CLI binary
│ ├── src/main.rs # REPL + file runner + format + compile commands
│ └── Cargo.toml
└── oo7-lsp/ # Language Server binary
├── src/main.rs # stdio transport, 6 LSP capabilities
└── Cargo.toml
linker/ # Linker (separate workspace member)
├── src/
│ ├── linker.rs # Core linker: symbol resolution, relocations
│ ├── oo7_format.rs # 007 IR JSON format
│ ├── relocation.rs # Relocation validation + resolution
│ ├── symbol.rs # Symbol representation
│ ├── section.rs # Section merging (canonical order)
│ ├── archive.rs # Unix .a archive generation
│ ├── security.rs # Type-safe FFI + symbol versioning
│ └── object_format.rs # Multi-format detection (ELF/Mach-O/COFF/WASM/007)
└── Cargo.toml
interpreter/ # Multi-language backend module
├── src/
│ ├── lib.rs # Backend registry + interpreter
│ ├── backend.rs # LanguageBackend trait
│ └── backends/rust.rs # Rust reference backend
├── idris2_abi/
│ └── BackendABI.idr # Idris2 ABI for backend FFI
└── zig_impl/ffi.zig # Zig FFI: C-compatible backend interface
proofs/
├── idris2/
│ ├── Harvard.idr # Harvard invariant, budget monotonicity, LinearHandle QTT ✓ checked
│ ├── TropicalSemiring.idr # Semiring laws for cost model ✓ checked
│ ├── CNO.idr # Certified Null Operations ✓ checked
│ ├── TypeSoundness.idr # Progress + preservation (closed + open terms) ✓ checked
│ ├── SessionDuality.idr # Session type duality, 2-party projection ✓ checked
│ └── Determinism.idr # evalData determinism + environment independence ✓ checked
└── lean4/ # Proof obligation templates
editors/
└── vscode-007/extension.js # VS Code extension + PanLL trace panel
| Tier | Purpose | Backends |
|---|---|---|
| 0 | Core | 007, DSL, JSON, Elixir-validator, Shell |
| 1 | High-value | BEAM, Idris2, VeriSimDB, LLM, Zig FFI |
| 2 | Ecosystem | Gleam, ReScript, Nickel, Scheme, WASM |
| 3 | Infrastructure | HTTP, SQL, Groove, PanLL, Containerfile |
| 4 | Research | Lean4, Tropical semiring, Epistemic logic, Choreography |
| 5 | Coprocessors | CUDA, Vulkan, Metal, OpenCL, FPGA, TPU, DSP |
Mature Rust-side compilation path from the 007 AST to source/IL targets.
| Backend | Output | Targets | License |
|---|---|---|---|
| Elixir/OTP | .ex source | BEAM VM | PMPL |
| WASM | .wat modules | WebAssembly | PMPL |
| Zig | .zig source | x86/ARM/WASM/RISC-V (via Zig) | PMPL |
| QBE | QBE IL text | x86_64/AArch64/RISC-V (via qbe binary) | MIT |
| Cranelift | .o object files | x86_64/AArch64/RISC-V (pure Rust) | Apache-2.0 |
| Idris2 | .idr source | Proof obligations | PMPL |
| Lean4 | .lean source | Proof obligations | PMPL |
Native Zig-side compilation path from the Zig parser IR to binary/source targets.
Only twasm is on the verified path. All others are RAW emitters kept for
pipeline smoke tests and experimentation — they earn no safety claims.
| Backend | Output | Status | Notes |
|---|---|---|---|
| twasm | typed-wasm source (.twasm text) |
VERIFIED (lands task #3) | The only verified codegen path. Feeds typed-wasm L1-L10 checked core; L13-L16 as those levels land. |
| x86 | minimal ELF64 byte stream | RAW — non-linkable | Stage-2 body compilation, no section headers / symbol table / relocations. Not loadable by ld/lld. |
| arm | flat AArch64 binary (007 header) | RAW — non-standard | Stage-2 body compilation, non-ELF private header. Not linkable by system tools. |
| wasm | raw Wasm MVP module | RAW — no type layer | Valid .wasm but no typed-wasm regions / schemas / effects. Superseded by twasm once task #3 lands. |
Selecting --target x86 | arm | wasm prints a "not verified" warning to stderr.
Selecting --target twasm before task #3 errors with TwasmBackendNotYetImplemented
— no silent fallback.
See compiler-core/zig/src/codegen/codegen.zig for the canonical backend-status
table (Target.is_verified, Target.label) and the llm-warmup-dev.md for the
rationale behind typed-wasm-first.
| File | What it proves |
|---|---|
| Harvard.idr | DataExpr cannot contain ControlExpr (by construction) |
| Harvard.idr | Data Language evaluation terminates (totality checker) |
| Harvard.idr | Linear handles consumed exactly once |
| Harvard.idr | Budget spend can't overspend |
| TropicalSemiring.idr | (TropNat, min, +) is a commutative semiring |
| TropicalSemiring.idr | @total functions have zero cost (multiplicative identity) |
| CNO.idr | Empty program is a CNO |
| CNO.idr | Halt is a CNO |
| CNO.idr | eval distributes over program concatenation |
| CNO.idr | CNO cost = Finite 0 in tropical semiring |
| TypeSoundness.idr | Progress: every closed DataExpr terminates with a typed value |
| TypeSoundness.idr | Preservation: evaluation preserves types (closed + open terms) |
| TypeSoundness.idr | openPreservation with semantic EnvCoherence hypothesis |
| SessionDuality.idr | dual is an involution (dualInvolution) |
| SessionDuality.idr | 2-party global projections produce dual local types |
| SessionDuality.idr | dualSymmetric, muDual for recursive session types |
| Determinism.idr | evalData is deterministic (trivial — Refl) |
| Determinism.idr | Closed terms are environment-independent (closedEnvIndep) |
| Determinism.idr | Closed terms evaluate identically in empty environment |
| Benchmark | Standard | Algebra-matched | Speedup |
|---|---|---|---|
| Graph reachability (32 nodes) | 70.6 µs | 2.7 µs (boolean bitwise) | 27x |
| Probability chain (1000 terms) | 1.88 µs (underflows!) | 1.42 µs (log-semiring) | 1.3x + correct |
| Shortest path (64 nodes) | 1.19 ms (Dijkstra) | 5.21 ms (tropical) | Dijkstra wins |
| CRC-32 (4KB) | 12.3 µs (table) | 25.8 µs (GF(2)) | Table wins on CPU |
- Upstream: JTV (Julia the Viper) — addition-only Data Language heritage
- Upstream: absolute-zero — CNO theory (92 Coq proofs)
- Downstream: Hypatia (neurosymbolic scanning), PanLL (panels), VeriSimDB
- Specification:
spec/grammar.ebnf(1127 lines),spec/LANGUAGE-SPEC.adoc,spec/TYPE-SYSTEM-SPEC.adoc
- Container: Stapeln (Chainguard base)
- CI/CD: GitHub Actions + Hypatia scan
- Development: Nix flake / Guix shell / direnv