has someone explored the concept of verified sandboxing? imagine if WASM programs could be annotated with correctness proofs, which would be verified by the runtime and would then allow less (or no) sandboxed operation
@mildsunrise Hmm. This doesn't sound like object capabilities, but you may be interested in them anyway if you're thinking about sandboxing. I liked this intro on it
@mildsunrise From the other posts in the thread this actually sounds even less related than I might have thought. I was thinking more on how it lets you reason on a high level what a program or parts of it can and can't do, but you're talking about memory pointers and stuff
