Re:Extism: Make all software programmable with WebAssembly
by titzer on Thursday December 01, 2022 @11:08AM
(#33818193)
> 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!
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!