Sounds unpleasant. There are loads of ways of maintaining this property without resorting to formal verification. Hardware is already largely verified, thankfu

Sounds unpleasant. There are loads of ways of maintaining this property without resorting to formal verification. Hardware is already largely verified, thankfully, and where formally verified software exists it is probably good to use, but in general? You wouldn't have to worry about code bloat for sure; it'd take weeks to write every line of code! The problem is that this sort of code has to be writable by exclusively average developers, and proof assistants just aren't at that level yet (and might never be). A verified implementation of the register colouring algorithm (100 lines of C, perhaps) takes 10,000 lines of code. Useful, yes, but not practical, especially for a whole OS.