I think you answered your own question (to some extent). Rewriting the necessary protocols/libraries in a type-safe manner already provides an improvement over the current systems. In addition, (with the standard approach) it's quite hard for a developer to reason about the whole stack they're using and privilege escalation bugs are particularly irksome. Writing the applications with the approach Mirage takes means that there is less code to reason about.
An anecdote I use when describing the benefits is the story of a smart fridge that got hacked and became part of a botnet sending spam emails. Why did that fridge even have code that allowed it to send email? It wasn't necessary for its functioning. We should write software differently if were going to be deploying it to 10x the number of devices compared to today.
More personally, I worry about the software that's going to find it's way into the embedded health devices of the future (cf pacemakers). These devices will inevitably be 'connected' and I want to make sure that the code they use is safe and secure.
> Why did that fridge even have code that allowed it to send email?
If it has a remote code execution vulnerability, it's trivial to make it send spam (or do all kinds of things) whether a MUA was already present or not.
An anecdote I use when describing the benefits is the story of a smart fridge that got hacked and became part of a botnet sending spam emails. Why did that fridge even have code that allowed it to send email? It wasn't necessary for its functioning. We should write software differently if were going to be deploying it to 10x the number of devices compared to today.
More personally, I worry about the software that's going to find it's way into the embedded health devices of the future (cf pacemakers). These devices will inevitably be 'connected' and I want to make sure that the code they use is safe and secure.