Proof assistant kernel, not operating system kernel - in case, like me, you clicked in hoping to debate the merits of microkernels vs monolithic:) Although I suppose there is a significant analogy, since the argument here... if I understood right... is very close to the classic 'and now a small defect in a device driver just panicked the system or gave an attacker root', just in math terms.
Yes, the analogy might help. Though as far as I know the common OS kernel reply 'we have to stick it all in the kernel to achieve performance' doesn't apply to proof assistants.
3 comments