Commit 3f14884
feat(groove): add companion paper — Typing the Boundaries
"Typing the Boundaries: Preserving Type Safety Across Every System
Crossing Point" — companion paper to the Groove Protocol paper.
Thesis: the world is typed at the edges and untyped in the gaps.
Types don't need to die at system boundaries if the boundaries
themselves are typed.
Six boundary categories with mechanisms:
1. Language (ABI/FFI/API triple, roundtrip proofs)
2. Service (Groove Protocol, structural subtyping)
3. Protocol (Typed Frame Router, transparency proofs)
4. Component (FLI, clade-based trait matching)
5. Runtime (Browser harness, CORS + type chain)
6. Storage (VeriSimDB, 8-modality drift detection)
Key results:
- Boundary Composition theorem: chained boundary proofs compose
via transitivity — types survive multi-boundary crossings
- Five of six mechanisms have zero runtime cost (proofs erased)
- Three boundaries that cannot be typed (WAN, encrypted mid-stream,
broadcast) identified as limitations
- "Why Now" section: Idris2 QTT + Zig zero-overhead FFI + IPv6
link-local convergence enables this for the first time
Targets: arXiv cs.PL/cs.SE/cs.NI, subsequently POPL/OOPSLA/NSDI
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>1 parent df0add7 commit 3f14884
1 file changed
Lines changed: 585 additions & 0 deletions
0 commit comments