(author of the post here)
Hey Berké! I remember your talk very well (I was in the room), super interesting and it really got me thinking about this area!
Since then, the more I look into it, the more I see a fit with our MirageOS unikernel work. On the ground, you can paper over security and specialisation by throwing more machines (or money) at the problem. In orbit you cannot, so both the compile-time and the runtime guarantees have to be right!