Skip to content

ROADMAP.adoc

Latest commit

 

History

History
187 lines (152 loc) · 9.61 KB

ROADMAP.adoc

File metadata and controls

187 lines (152 loc) · 9.61 KB
Raw

typed-wasm Roadmap

Relation to the production path

This roadmap tracks specific version milestones (v0.1.0 …​ v1.0.0). The long-form strategic plan — six phases from pre-alpha to production-ready, with explicit gates, load-bearing decisions, and a comparison landscape — lives in docs/PRODUCTION-PATH.adoc. The two documents stay in sync as follows:

Version axis (this file) Phase axis (docs/PRODUCTION-PATH.adoc)

v0.1 — v0.4

Phase 0 (stabilize foundation)

v1.0

Phase 1 (end-to-end producer)

v1.x

Phase 2 (multi-producer adoption)

v2.0 (planned)

Phase 3 (runtime-side enforcement)

v2.x — v3.0

Phases 4-5 (tooling, spec, standards)

v3.x stable

Phase 6 (production hardening)

When this roadmap says "complete" it means a specific deliverable shipped. When PRODUCTION-PATH.adoc says "gate met" it means an entire phase’s preconditions are satisfied and the next phase can credibly begin. The two views diverge intentionally: version cuts can happen mid-phase; phase transitions usually require multiple version cuts to accumulate.

Current State

typed-wasm applies a checked TypeLL-derived 10-level core to WebAssembly linear memory. Pre-alpha / research stage. Core insight: WASM linear memory is a schemaless database; typed-wasm adds region schemas and typed access operations.

Killer feature: multi-module shared memory type safety across language boundaries (e.g. Rust Module A shares WASM memory with AffineScript Module B — neither source type system covers the boundary; typed-wasm does).

Key capabilities delivered:

  • Idris2 ABI proofs (src/abi/) — checked L1-L10 region, access, and proof core

  • Zig FFI (ffi/zig/) — C-ABI bridge for runtime region management, typed load/store

  • .twasm grammar (spec/grammar.ebnf) — EBNF surface syntax

  • 10-level spec (spec/type-safety-levels-for-wasm.adoc) — checked DB-to-WASM core mapping

  • Example .twasm files for the checked core, plus draft higher-level examples

  • Whitepaper drafts (docs/WHITEPAPER.md + docs/arxiv/typed-wasm.tex) under audit

  • No unsound escape hatches in the checked Idris2 core (believe_me, assert_total)

  • Estate-axis accommodation (A15/A16, 2026-06-16): L11/L12/Echo now cross-document and mirror the canonical estate repos — tropical-resource-typing (Lean4 Resource.*: dioid order, MinMax/hubCeiling bottleneck, ResidueMeasure), echo-types (Echo re-characterised as a tropically-graded loss modality; EchoR/echoToResidue), epistemic-types (additive syncGrade). The min-plus grade is one shared object across all three. See LEVEL-STATUS.md "Estate-axis accommodation". Three upstream drafts prepped local/unpushed for owner review.

Known audit constraints:

  • L11 (Tropical) and L12 (Epistemic) are in typed-wasm.ipkg since 2026-04-18 (commit A1) and build clean under Idris2 0.8.0 (PROOF-NEEDS.md reconciliation 2026-05-18). Treat them as research/draft for surface semantics, not for ipkg membership. (A15/A16 2026-06-16 added the canonical estate cross-doc
    order/bottleneck/residue/sync-grade mirrors; the monad/comonad/adjunction variance of the echo grade remains deferred to upstream --safe Agda.)

  • Release/build/container metadata still contains template residue

  • Benchmark and venue-facing paper claims require evidence cleanup before submission

v0.1.0 — Formal Foundations (Complete)

  • ✓ Idris2 ABI: region schema proofs

  • ✓ Idris2 ABI: typed access proofs

  • ✓ Idris2 ABI: checked 10-level verification hierarchy

  • ✓ Zig FFI: runtime region management

  • ✓ Zig FFI: typed load/store operations

  • ✓ .twasm EBNF grammar

  • ✓ 10-level specification document

  • ✓ Example .twasm files

  • ✓ Multi-module shared memory type definitions

v0.2.0 — ECHIDNA Integration (Complete — 2026-03-29)

  • ✓ Property-based testing of proof soundness via ECHIDNA Prover Wars

  • ✓ Random .twasm program generation (tests/echidna/echidna-harness.mjs)

  • ✓ Prover oracle testing (ffi/zig/test/echidna_oracle_test.zig — 7 properties)

v0.3.0 — Submission Drafts (In revision)

  • ✓ Formalise whitepaper for arXiv submission (docs/arxiv/typed-wasm.tex — ACM sigplan format)

  • ✓ BibTeX bibliography (docs/arxiv/typed-wasm.bib — 15 references)

  • ❏ Benchmark multi-module type checking overhead with reproducible artefacts

  • ✓ Comparison with existing WASM safety approaches (Section 8, Table 6)

  • ❏ Reconcile all paper claims with the checked L1-L10 evidence envelope

  • ❏ Submit to arXiv / HAL only after claim and benchmark audit passes

v0.4.0 — Ecosystem Integration (Partially Complete)

  • ✓ TypedQLiser plugin (WASM as a "query target") — typedqliser/src/plugins/wasm.rs (541 lines)

  • ❏ VCL-total sibling integration (same levels, different domain)

  • ❏ GraalVM/Truffle target (multi-language shared state type safety)

  • ✓ typed-wasm-verify Rust crate (crates/typed-wasm-verify/) — post-codegen L7+L10 verifier. Consumed by hyperpolymath/ephapax as of 2026-05-15 (compile --verify-ownership); hyperpolymath/affinescript migration from its in-tree OCaml verifier deferred to v1.0.

v1.0.0 — Stable Release

  • ❏ Complete .twasm parser (beyond EBNF grammar)

  • ❏ End-to-end pipeline: .twasm source → verified WASM module

  • ❏ Multi-language binding generation from typed region schemas

  • ❏ CI/CD with proof validation

  • ❏ De-template release/build/container surfaces

  • ❏ Real benchmark and aspect-test evidence

  • ✓ Post-codegen verifier in Rust (crates/typed-wasm-verify/) — partial v1.0 deliverable, the verifier side of the pipeline. Parser/checker for .twasm source remains the open work.

  • ❏ Cross-compat parity proof against hyperpolymath/affinescript:lib/{tw_verify,tw_interface}.ml — real OCaml-emitted .wasm fixtures alongside the existing synthetic ones (deferred to "C5.1").

Language Identity & Linguist Classification

typed-wasm is a type discipline over WebAssembly, not a separate bytecode format. The .twasm surface syntax elaborates to standard WASM modules after the L1—​L10 checks fire. This shapes how the project should be classified by external tooling (GitHub Linguist, tree-sitter, LSP clients, editor plugins).

Current classification (v0.1.x)

  • .gitattributes maps *.twasm to linguist-language=WebAssembly via an override. Rationale: Linguist has no "Typed WebAssembly" entry, and without the override Linguist runs content heuristics on files that start with // comments — producing nondeterministic misclassification (C, C++, JavaScript, or plain Text). The override guarantees .twasm files are counted as WebAssembly in the GitHub language bar and keeps the repo’s external fingerprint stable.

  • Trade-off: this under-claims the typed-ness. A reader browsing GitHub sees "WebAssembly" and has no cue that the files encode a 10-level type discipline. That is acceptable for a pre-alpha research repo; it is not acceptable at v1.0.0.

Path to distinct Linguist language (v1.0+)

Submitting "Typed WebAssembly" as a first-class Linguist language requires several preconditions that we do not yet meet:

  • ❏ Stable .twasm grammar beyond EBNF. Linguist accepts TextMate grammars (.tmLanguage.json) or references to published tree-sitter grammars. Neither exists yet. Blocker: port spec/grammar.ebnf to one of these formats.

  • ❏ tree-sitter-twasm repository with a published grammar and sample corpus. Required for editor tooling and also the cleanest input to a Linguist submission.

  • ❏ Evidence of adoption. Linguist’s contribution policy requires a language be in "actual use" — historically interpreted as a few hundred public repos with non-trivial content. A research repo with six example files will not clear this bar; seeding the estate to manufacture adoption is also not acceptable and will be noticed.

  • ❏ A settled answer on whether "Typed WebAssembly" should be a top-level language or nested under WebAssembly as a group. Nesting is the honest choice — typed-wasm is a conservative extension and its artefacts remain valid WASM — and it preserves the existing language bar semantics.

  • ❏ PR against github-linguist/linguist adding the language entry, sample files, and grammar reference. Expect multiple review cycles.

Tracking: this is tied to the v1.0.0 "Complete .twasm parser" milestone. The parser, the tree-sitter grammar, and the Linguist submission are the same piece of work viewed from three angles.

Adjacent language-tooling work (same precondition chain)

  • ❏ tree-sitter-twasm — grammar, parser, published NPM package

  • ❏ LSP server (twasm-lsp) — diagnostics surfacing L1—​L10 checks as editor squiggles rather than batch compiler errors

  • ❏ TextMate / VS Code syntax-highlight extension built from the tree-sitter grammar

  • ❏ Editor plugins: Helix, Zed, Neovim, Emacs (all derive from the tree-sitter grammar once it exists)

  • ❏ Browser-side .twasm validation tooling (requires a parser implementation reachable from JS/WASM)

These items are currently scattered under "Future" and v1.0.0; the common blocker is the grammar port, which should be scheduled before any of them.

Future

  • GraalVM compile-time guarantees replacing runtime InteropLibrary dispatch

  • Browser-side .twasm validation tooling (see Language Identity section; depends on tree-sitter-twasm)

  • Language server protocol support for .twasm files (see Language Identity section; depends on tree-sitter-twasm)

  • Linguist upstream submission (see Language Identity section; depends on grammar port and adoption evidence)