> proof-carrying code within Wasm That's a legitimately neat idea. There are couple of projects to improve safety of Wasm code using linear memory (such as Ric

> proof-carrying code within Wasm That's a legitimately neat idea. There are couple of projects to improve safety of Wasm code using linear memory (such as RichWasm by Amal Ahmed and MSWasm by a number of folks at Stanford, UCSD, and CMU). Obviously unrestricted aliasing of the giant byte array that is memory makes this more difficult. I hope that Wasm GC can offer an abstraction base to express even more invariants. In some sense that will be a study in adding more powerful types and more powerful proof constructs that are either on the side or embedded in the code. So, exciting future directions!