|
| 1 | +// SPDX-License-Identifier: PMPL-1.0-or-later |
| 2 | +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell |
| 3 | +:toc: macro |
| 4 | +:toclevels: 2 |
| 5 | +:icons: font |
| 6 | + |
| 7 | += Ephapax Roadmap |
| 8 | + |
| 9 | +_Linear-type language with dual formalisation (Coq + Idris2) targeting WebAssembly._ |
| 10 | + |
| 11 | +toc::[] |
| 12 | + |
| 13 | +== Current State |
| 14 | + |
| 15 | +Ephapax is an early-development linear-type language implemented across 19 Rust crates |
| 16 | +with a two-phase compiler pipeline (Idris2 type-checking -> Rust/WASM backend). The core |
| 17 | +type system design, lexer, parser, interpreter, REPL, and CLI are complete. The type |
| 18 | +checker and WASM code generation are in progress. |
| 19 | + |
| 20 | +**Dual formalisation status:** |
| 21 | + |
| 22 | +* **Coq** (`formal/`): `no_leaks` (Qed), `memory_safety` (Qed), `progress` (92%), |
| 23 | + `preservation` (50%). Three `Admitted` proofs remain: `ctx_transfer` (15/24 cases), |
| 24 | + `subst_lemma`, `preservation`. |
| 25 | +* **Idris2** (`src/formal/`): `noEscapeTheorem`, `regionSafetyTheorem`, `noGCTheorem`, |
| 26 | + `orthogonalityLemma` -- all complete with zero unsafe patterns. |
| 27 | + |
| 28 | +**Interpreter:** Environment-leak fix applied (2026-03-28). Proofs chain and effects |
| 29 | +chain are sound. |
| 30 | + |
| 31 | +== v0.1.0 -- Core Language (In Progress) |
| 32 | + |
| 33 | +* [x] Core type system design (affine + linear modes) |
| 34 | +* [x] Lexer (logos-based tokenizer) |
| 35 | +* [x] Parser (chumsky-based) |
| 36 | +* [x] Tree-walking interpreter with env-leak fix |
| 37 | +* [x] REPL |
| 38 | +* [x] CLI (`ephapax-cli`) |
| 39 | +* [x] Coq formalisation: `no_leaks` proof (Qed) |
| 40 | +* [x] Coq formalisation: `memory_safety` proof (Qed) |
| 41 | +* [x] Idris2 formalisation: all four theorems complete |
| 42 | +* [x] S-expression IR (`ephapax-ir`) |
| 43 | +* [x] Two-phase pipeline: Idris2 type-check -> Rust WASM backend |
| 44 | +* [x] Zig FFI token buffer (`Ephapax.Parse.ZigBuffer`) |
| 45 | +* [x] Conformance test suite (pass/fail cases) |
| 46 | +* [ ] Type checker completion (`ephapax-typing`) |
| 47 | +* [ ] WASM code generation: lambda/app compilation (closure conversion) |
| 48 | +* [ ] Coq: close `ctx_transfer` proof (9 remaining cases of 24) |
| 49 | +* [ ] Coq: close `subst_lemma` proof |
| 50 | +* [ ] Coq: close `preservation` proof (currently 50%) |
| 51 | +* [ ] Coq: `progress` proof completion (currently 92%) |
| 52 | + |
| 53 | +== v0.2.0 -- Backend Maturity |
| 54 | + |
| 55 | +* [ ] Closure conversion for WASM backend |
| 56 | +* [ ] Native backend via Cranelift |
| 57 | +* [ ] Region-based allocation in WASM linear memory |
| 58 | +* [ ] Bulk deallocation on region exit |
| 59 | +* [ ] Standard library foundation (`ephapax-stdlib`) |
| 60 | +* [ ] Surface syntax desugaring pipeline (`ephapax-desugar`) |
| 61 | +* [ ] Package system (`ephapax-package`) |
| 62 | +* [ ] LSP server (`ephapax-lsp`) -- basic diagnostics |
| 63 | + |
| 64 | +== v0.3.0 -- PipeWire Proving Ground |
| 65 | + |
| 66 | +PipeWire filter node as a real-world validation of linear types for audio buffer management. |
| 67 | + |
| 68 | +* [ ] PipeWire filter node implementation in Ephapax |
| 69 | +* [ ] Linear buffer types proving zero-copy audio safety |
| 70 | +* [ ] Real-time constraints validation (no GC pauses) |
| 71 | +* [ ] Integration with AmbientOps audio pipeline |
| 72 | + |
| 73 | +== v0.4.0 -- Tooling and Ecosystem |
| 74 | + |
| 75 | +* [ ] Tree-sitter grammar (`editors/tree-sitter-ephapax`) integration with editors |
| 76 | +* [ ] LSP server -- full features (hover, go-to-definition, completions) |
| 77 | +* [ ] Documentation generator (`ephapax-doc`) |
| 78 | +* [ ] VRAM cache for GPU-side linear resources (`ephapax-vram-cache`) |
| 79 | +* [ ] Static analysis module (`ephapax-analysis`) |
| 80 | +* [ ] Error recovery in parser for IDE use |
| 81 | + |
| 82 | +== v1.0.0 -- Production Ready |
| 83 | + |
| 84 | +* [ ] All Coq `Admitted` proofs closed (zero remaining) |
| 85 | +* [ ] Full `preservation` and `progress` proofs (Qed) |
| 86 | +* [ ] Stable surface syntax (already locked, but confirm no changes needed) |
| 87 | +* [ ] Comprehensive standard library |
| 88 | +* [ ] Cross-platform WASM + native compilation |
| 89 | +* [ ] Performance benchmarks vs Rust/C for linear workloads |
| 90 | +* [ ] Published language specification (`spec/`) |
| 91 | + |
| 92 | +== Long-Term |
| 93 | + |
| 94 | +* [ ] Session-sentinel integration (Ephapax rewrite of session management) |
| 95 | +* [ ] Gossamer integration for UI applications |
| 96 | +* [ ] IDApTIK migration from current stack to Ephapax where linear types add value |
| 97 | +* [ ] Self-hosting: Ephapax compiler written in Ephapax |
0 commit comments