This is kinda like saying if we had electric vehicles that can charge instantly and have million km range then everyone would switch. Sure, that's correct. But

This is kinda like saying if we had electric vehicles that can charge instantly and have million km range then everyone would switch. Sure, that's correct. But it totally glosses over the fact that something like that is just not possible to build in the foreseeable future. A kernel that rivals Linux in its feature set and is formally verified is even more of a bonkers proposition.