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.
> Proof assistant kernel, not operating system kernel
It's the neologism they use to own the word and define it however they want. The other one is 'harness' that I didn't even click to see what they want it to mean.
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.
> Proof assistant kernel, not operating system kernel
It's the neologism they use to own the word and define it however they want. The other one is 'harness' that I didn't even click to see what they want it to mean.
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.
Here is the postmortem of the lean bug: https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...
Previous related discussion: https://news.ycombinator.com/item?id=49137060