The WebAssembly Component Model proposal defines a standard, language-neutral, portable, and compositional way to specify interfaces for coarse-grained interoperation between WebAssembly modules and the host environment or other WebAssembly components written in a different language. The Component Model is layered on top of the Core WebAssembly specification, and provides both a way to specify how to link Core Wasm modules together to form a coarse unit of composition (which fully encapsulates primitive notions such as shared memories) and a way to specify high-level interfaces between such components, such as the WebAssembly System Interface.

This talk will introduce the Component Model and its design, as well as the formalism that underlies its specification, its basic metatheoretic structure, and how each major feature is presently formalized. It will also provide an overview of how the Component Model is compositionally layered on top of the Core WebAssembly specification, and leverages Core WebAssembly proposals, such as effect handlers, in its treatment of async functions and values.

The Component Model considered as a language is in an unusual position, as it is a linking and interface-specification language whose execution is interwoven with Core WebAssembly execution. Consequently, traditional language soundness theorems, such as syntactic type soundness, may be insufficient to capture interesting properties of the Component Model language. This talk will further discuss & invite discussion on this position, and the unique structures of soundness theorems, inspired by multilanguage semantics, that apply to this niche.