I wonder if this might be the push that functional programming + formal verification needs to hit the mainstream.
Compare Erlang, for example, which must have seemed needlessly complex and theoretical outside of modern super-horizontal-scale computing.
I understand that NASA, the #1 in "if this code breaks we all lose our jobs" driven development, are big into formal methods. I think applying that same rigor to smart microwaves wouldn't be such a bad thing.
The formal verification subject is tricky. For a lot of software (especially in the web startup world) it is often not possible to hire someone trained in formal methods to perform extensive checks/proofs on software which undergoes rapid change as the company pivots every couple of months.
Functional programming alone doesn't give you any guarantees about safer or more correct software than any object oriented language unless you ruthlessly exploit its type-system. Even if you do, the specs have to exist upfront and they have to be correct and stable.
One can make the case that isolating side effects and capsuling them in a controlled structure is "the right thing" to do, but that alone does not give you any formal verification of your program.
From personal experience I can only say that whenever I brought up formal verification because of security/correctness concerns, I was immediately shut down by business, because it's simply too expensive for software that doesn't control life-critical systems.
I think with security (and esp. privacy), the problem is more coming up with the specs in the first place. If you can do that in a reliable way, designing appropriate static analyses is probably doable.
Compare Erlang, for example, which must have seemed needlessly complex and theoretical outside of modern super-horizontal-scale computing.
I understand that NASA, the #1 in "if this code breaks we all lose our jobs" driven development, are big into formal methods. I think applying that same rigor to smart microwaves wouldn't be such a bad thing.