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.
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.
Previous related discussion: https://news.ycombinator.com/item?id=49137060
Here is the postmortem of the lean bug: https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...