News for hackers. Stuff that matters.
Re:Hyperkernel – A push-button approach to building provably... by ajb on Wednesday September 12, 2018 @06:06AM (#17966993)
Formal verification arrived at hardware first, really. Because although sofware and hardware can in principal be equally complex, the economic cost of a bug in hardware causes as much as possible of the complexity to be punted into software. That leaves the problem of verifying hardware more tractable. I don't think it's yet done comprehensively but a greater fraction of forma verification is used on hardware than software.
Re:Hyperkernel – A push-button approach to building provably... by Filligree on Wednesday September 12, 2018 @06:13AM (#17967021)
That's also a large part of the push towards microcode. Once you get to the level of micro-ops, even modern CPUs are... reasonably simple.

The flip side is, your CPU may need a firmware update. >_>