You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
docs+meta: wiki source-of-truth + STATE.a2ml updated for Phase 0 closure (#61)
## Summary
Phase 0 documentation update for **humans (wiki) and machines
(`.a2ml`)**.
## Wiki (`docs/wiki/`)
The GitHub wiki at `hyperpolymath/typed-wasm/wiki` had stale content
(PMPL license, pre-restructure proof paths, no mention of
production-path or current state). Sandboxed sessions can't write to the
wiki repo directly — signing infrastructure is scoped to
`typed-wasm.git`. So wiki content is now sourced from `docs/wiki/` in
this repo with a documented sync workflow.
| Page | Purpose |
|---|---|
| `Home.md` | Landing — current state, 10-level table, killer feature,
quick start, sibling projects, **MPL-2.0 license corrected** |
| `Production-Path.md` | The 6-phase plan (companion to
`docs/PRODUCTION-PATH.adoc`) |
| `Phase-0-Status.md` | Live closure state with PR cross-links + test
surface summary; documents which Phase 0 gates are met |
| `Comparison.md` | Landscape vs MS-Wasm / CHERI-Wasm / wasmGC /
AssemblyScript / Rust / CompCert at each maturity level |
| `README.md` | Sync workflow + authoring rules |
To deploy: `cp docs/wiki/*.md ~/twasm-wiki/ && cd ~/twasm-wiki && git
add -A && git commit -m "Sync from typed-wasm" && git push`
## STATE.a2ml (machine-readable)
Comprehensive update for the Phase 0 closure pass — was anchored to
2026-04-12. Highlights:
- `last-updated` 2026-04-12 → 2026-05-24
- `completion-percentage` 55 → 70
- New keys: `production-phase = "0"`, `production-phase-status` with
3-gate breakdown
- Milestone deltas:
- Parser/Zig/smoke 80 → 100
- De-template release metadata 15 → 60 (PR #57's security.txt + SPDX
fixes)
- Benchmarks + aspect coverage 10 → 70 (property + security-envelope +
proof-regression in PR #57)
- 4 new milestones added: production-path doc + tracking issues,
tree-sitter scaffold (20%), CI persistent-reds hardening, ROADMAP
truthfulness audit
- `last-result` warn → pass
- New `[test-surface]` section enumerating **545 assertions across 11
surfaces**
- New `[tracking-issues]` section mapping each phase to its GitHub issue
- `ecosystem.depends-on` removed ReScript (being-removed); added
`ships-to` for AffineScript + Ephapax
## Files
- `docs/wiki/Home.md` — new
- `docs/wiki/Production-Path.md` — new
- `docs/wiki/Phase-0-Status.md` — new
- `docs/wiki/Comparison.md` — new
- `docs/wiki/README.md` — new (sync workflow)
- `.machine_readable/6a2/STATE.a2ml` — comprehensive update
No code changes.
## Test plan
- [ ] Markdown renders cleanly when synced to wiki repo
- [ ] STATE.a2ml parses as valid TOML
- [ ] No regressions in existing test surfaces (no code changed)
- [ ] All PR cross-links in `Phase-0-Status.md` resolve
---
_Generated by [Claude
Code](https://claude.ai/code/session_01ExgUTJmU5UQQNLKynwxDjm)_
@@ -21,7 +21,9 @@ Two first-class roles (ADR-004):
21
21
(both compile to WasmGC). Provides formally verified type layout and ABI
22
22
conventions so cross-language calls require no marshalling layer.
23
23
"""
24
-
completion-percentage = 55
24
+
completion-percentage = 70 # bumped from 55: foundation defensibly engineered; codegen pipeline kickoff complete; CI honest; 545+ test assertions across 11 surfaces; ROADMAP truthful with drift-detection aspect in place
25
+
production-phase = "0" # see docs/PRODUCTION-PATH.adoc — phase 0 of 6
26
+
production-phase-status = "2 of 3 gates met (gate 1: CI green-or-advisory ✓; gate 2: codegen v0 ✗; gate 3: ROADMAP truthful ✓)"
"Track B: open AffineScript session, swap lib/{tw_verify,tw_interface}.ml for subprocess call to typed-wasm-verify binary.",
72
+
"Investigate Build+E2E root cause once authenticated log access available; replace idris2 install with idris2-pack or build-from-source.",
60
73
"L11-modal-box: integration test with TypeLL L10 context; QTT semantics review before graduation.",
74
+
"ADRs for the 6 load-bearing decisions D1-D6 from docs/PRODUCTION-PATH.adoc §'Load-bearing decisions' (especially D2: producer-side-only vs runtime-aware, which gates whether Phase 3 happens).",
Where typed-wasm sits among neighbouring approaches at each maturity level. Approximate; the wasm-safety landscape moves fast.
4
+
5
+
## Today (early Phase 0, ~v0.1)
6
+
7
+
Honest peer set: **academic research prototypes for wasm memory safety**.
8
+
9
+
| Project | What it does | typed-wasm comparison |
10
+
|---|---|---|
11
+
|**MS-Wasm** (Disselkoen et al. 2019+) | Segmented memory model, runtime enforcement of bounds, hot/cold heap separation | Closest peer in ambition. typed-wasm is **stronger in formal foundation** (Idris2 proofs vs. paper proofs), **weaker in deployment** (no published runtime), **broader in scope** (L7–L10 reach beyond bounds) |
12
+
|**CHERI-Wasm** (Watson et al.) | Capability-machine extension for wasm, hardware-level enforcement | Different threat model. CHERI = runtime-hardware. typed-wasm = compile-time-discipline. Complementary, not competing |
13
+
|**WAVM / wasm-validate / wasmparser**| Well-formedness validators | typed-wasm is strictly stronger: every typed-wasm-valid program is wasm-valid, but not vice versa. Different niche |
14
+
|**AssemblyScript runtime**| Managed types + GC over linear memory | Same "type safety for wasm" niche, opposite angle (managed types vs. linear-region discipline). Production-deployed; typed-wasm is not |
15
+
|**Lucet** (Fastly, archived) | Sandbox isolation for wasm-as-FaaS | Different concern (host safety, not producer-side memory discipline) |
16
+
17
+
At start of Phase 0, typed-wasm sits roughly where MS-Wasm was at its initial publication: a credible academic prototype with formal claims and a verifier, lacking the runtime story and production deployment. It would be the **only** entry in that peer set with machine-checked end-to-end proofs (the others have paper proofs or are unverified).
18
+
19
+
## After Phase 0 (foundation stabilized, ~v0.2)
20
+
21
+
Still a research prototype, but a **defensibly engineered** one. CI is honest; codegen v0 works for the simplest example; the ReScript-to-Idris2 parser migration has happened; the AffineScript adoption is real and working. Peer set unchanged but typed-wasm has moved from "interesting paper-ware" to "interesting paper-ware you can build and run without hand-holding".
22
+
23
+
This is *not yet* "a fully legit and working verified soundness discipline for wasm linear memory" in any sense an outsider would recognise. It is a credible research vehicle.
24
+
25
+
## After Phase 1 (end-to-end producer, ~v0.5 beta)
26
+
27
+
First version that warrants the description "**a working compile target with verified soundness for linear memory**". A user can take a `.twasm` source, compile it, and trust the 10-level discipline.
28
+
29
+
Peer set shifts: typed-wasm becomes comparable to **AssemblyScript** as a language-with-a-wasm-toolchain, but with a much stronger safety story. Still pre-1.0; still single-maintainer; still ecosystem-confined.
30
+
31
+
## After Phase 2 (multi-producer adoption, ~v0.9 RC)
32
+
33
+
typed-wasm enters the same category as **wasm-bindgen** (the standard "wasm + multi-language interop" surface) but with formal guarantees on top.
34
+
35
+
Three independent producers exist; the spec is stable enough that the second and third adoptions did not require spec changes. At this point typed-wasm is "**the standard way to opt into formal memory safety for any wasm producer**". Peer set: it has no direct peer at this maturity level; the closest comparison is **CHERI's adoption status** in the hardware world (specified, multi-vendor, used but not pervasive).
36
+
37
+
## After Phase 3 (runtime-side enforcement, ~v1.0)
38
+
39
+
typed-wasm becomes one of a small set of **memory-safe wasm-class platforms** with both producer- and runtime-side enforcement. Peer set:
|**MS-Wasm production runtime** (hypothetical) | If MS-Wasm reaches production by then |
45
+
|**wasmGC**| Different threat model (managed types) but addresses overlapping concerns from the other direction |
46
+
47
+
Within this set, typed-wasm's distinguishing claim is **the formal proof of soundness of its level discipline** (Idris2). CHERI has hardware proofs; wasmGC has wasm-spec coverage; MS-Wasm has paper proofs. typed-wasm would be unique in carrying machine-checked end-to-end proofs from spec to producer to runtime.
48
+
49
+
## After Phase 6 (production-hardened, v1.x stable)
50
+
51
+
Honest comparison is no longer to other wasm-safety projects but to **memory-safe systems languages and runtimes** in general:
52
+
53
+
| Project | Approach | What typed-wasm-1.x uniquely offers |
54
+
|---|---|---|
55
+
|**Rust**| Borrow-checker as producer-side memory safety | Rust is single-language; typed-wasm covers *any* wasm producer |
56
+
|**CHERI / Morello**| Hardware capability machine | CHERI is hardware-specific and per-runtime; typed-wasm is verifier-mediated and works on commodity hardware |
57
+
|**Pony reference capabilities**| Actor language with explicit ownership types | Pony is single-language; typed-wasm is producer-agnostic |
58
+
|**CompCert**| Verified C compiler with formal proofs | CompCert covers C → assembly; typed-wasm covers (any compiler) → wasm with stronger linearity claims |
59
+
|**wasmGC**| Managed types at the runtime level | wasmGC sidesteps linear memory; typed-wasm types linear memory directly |
60
+
61
+
typed-wasm at Phase 6 would occupy a distinct cell that **no existing system covers in one package**: machine-checked, verifier-mediated, runtime-enforced memory safety for **any wasm producer** with **cross-language sharing** verifiable end-to-end.
62
+
63
+
The closest analogue would be "Rust + CHERI + wasm" composed by hand — which no one ships as a product because the integration work is enormous and the formal coherence isn't there.
64
+
65
+
## The concrete impossibility today
66
+
67
+
If you wanted today to write a system where a Rust module and an OCaml module share wasm linear memory and you wanted machine-checked safety across that boundary, **no shipping toolchain gives you that**:
68
+
69
+
- Rust gives you borrow-checking inside Rust
70
+
- CHERI gives you runtime capability enforcement (if you have the hardware)
71
+
- MS-Wasm gives you bounds
72
+
- wasmGC sidesteps the question by using managed types instead
73
+
74
+
typed-wasm at Phase 6 is the first toolchain where that scenario works with formal guarantees.
75
+
76
+
## The honest read
77
+
78
+
typed-wasm is **uniquely positioned but unfinished**. The intellectual asset (the proofs, the 10-level discipline) is already world-class — there's nothing else with this depth of formalisation for wasm memory. The engineering surface around it is pre-alpha.
79
+
80
+
The [Production-Path](Production-Path) plan is the path from "world-class proof of concept" to "production toolchain with that proof of concept as its kernel". Phase 0 closes the engineering-fragility gap. Phase 1 makes it usable. Phases 2–6 take it to the maturity tier you'd want for shipping production wasm.
81
+
82
+
If you stop at end of Phase 1, you have "a Rust-borrowck-quality discipline you can opt any wasm producer into" — already a serious contribution. Phases 2–6 turn that into "an industry-recognised standard with multiple implementations and case studies".
0 commit comments