RichWasm: Bringing Safe, Fine-Grained, Shared Memory Interoperability to WebAssem...
summary
RichWasm is a higher-level WebAssembly dialect with a capability-based type system that enforces fine-grained, cross-language shared-memory safety: it models two global memories — unrestricted memory (GC) and linear memory (manual/ownership) — and capability types that forbid stashing a linear Rust pointer into an OCaml cell. The design is formalized and machine-checked in Coq with progress and preservation proofs, compiles by erasing types to core Wasm, and already catches the ownership bug shown in the example.
AI-written summary · about
chapters (10)
- 0:00RichWasm introduction
- 1:03WebAssembly memory limits
- 3:53Cross-language safety issues
- 7:29RichWasm design
- 15:44Capability types and memory
- 21:41Garbage collection in RichWasm
- 26:15Typing judgments and semantics
- 29:54Fixing interop example
- 30:56Future directions and Rust
- 33:46Q&A
related talks
21mRichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly
26mMemory Safety Preservation for WebAssembly
32mAll The Memory Safety Of C Combined With All The Blazing Speed Of JavaScript
25mMSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code
22mThe state of WebAssembly
43mMeet Your Future - WebAssembly
37mBuilding a better web with WebAssembly at the edge
01h 08mOn WebAssembly