3 ms·
The bugs are shifted into the spec, or the proof.
by hnfong 3y ago
The bugs are shifted into the spec, or the proof.
- snvzz 3y agoNot really shifted. If you think about it, a bug in the proof will require a bug in the code. This visibility is a good thing. Overall, note that the critical code, such as the microkernel itself, is small (kLoC wise) to begin with, which minimizes the odds a bug will go undetected for long.