Wouldn't that be somewhat outside of Theseus' design and add overhead more akin to modern OSes? Theseus relies on Rust's type system (ownership/borrowing and otherwise) to ensure that all binaries have many verified properties; arbitrary WASM program can't hook into that, yes?

The vast majority of programs running on a user's computer today are already running in a VM (JS and WASM), and the number is only increasing. I do not know of any argument in behalf of running everything in a VM (even when it's not a requirement) from a cybersecurity perspective, but I suspect there may be one.

You're right, but maybe this is the way to go and the tradeoff to accept. After all, the ideas behind Theseus feel so obviously correct, alike to those of Nix.