That poor guy who thought that he'd have to invent a new language to solve his sucky elevator's problem should've looked around instead. There's about 30 years of experience, languages, and tooling available to solve problems like this: synchronous languages. Rust may be good for other use cases but as long as it doesn't have a verified compiler (such as CompCert or CakeML) and a usable proof theory I'm not going to touch it except for hobbyist purposes. What it does for memory safety I can do without even thinking too hard in C. And then I could prove it. In Rust, I'd have to believe a compiler that's just a toy.

You're right about such an OS to exist already, you merely got its name wrong. It is called seL4.

(Disclaimer: I had my fingers in that pie.)

But can we really? Do we expect our old and frail citizens to achieve what we typically can't, namely tame our ill-behaving devices? Think about it. When those wonderful "things" are bored from talking grandpa into taking his medicine they help other people with running a DDoS. And while doing that they conveniently forget what they were supposed to do for grandpa. I for one am not looking forward to all those sad news items about dead bodies in "modern" homes.

Why do I have to read about other people's pedestrian shopping problems on a "news for nerds" site?

..because it assumes only rational agents.