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.
Yeah in theorem provers usually the opposite is true: "We want to put as little stuff as possible in the kernel because that's the part we need to verify by hand"
No, that is true, even if not uniquely. A kernel bug can easily bring down the machine. Maybe Xorg can also manage it... although IMHO that also sounds like a kernel bug (surely it's the kernel's job to ensure no user program can do that?)... but that doesn't make the kernel safe. And I suspect it's easier to take down the machine from ring 0 than a display server even if both can do it.
A kernel panic doesn't bring down the CPU, nor the hard drive, or the RAM, or the power supply unit. So if we're being pedantic, the machine is still up.
Well, a kernel bug gets write access to everything. A bug in userland is a bit more constrained in what it can do.
That counts especially for accidental bugs and denial of service. To make a userland bug exploited adversarially not impact the rest of the system requires more hardening of the kernel.
Yes, these are the standard excuses. But has anyone actually thought about them in the last twenty years, in the context of the way we actually use computers?
Eh, yes? Just look the discussions surrounding the development of any web browser? Or look at the permissions system in Android or iOS or on Mac (and perhaps even Windows?).
I think in the background of article's premises is an argument about classical vs. intuitionistic logic, rather than only about the merits of putting stuff in the kernel vs. outside.
Isabelle seems to use classical logic and set theory. Classical logic is often simpler, but when you do the "hard toil" (as the article puts it) of building recursive functions on set theory, all you've really done is to nonconstructively prove the existence of a set of pairs with certain properties. Good luck evaluating such an abstract "existence" with any concrete argument. Whereas intuitionistic logic as used by Coq is more complicated, but that's in part because its notion of "function" is an actual procedure in your computer that can accept an argument and produce a result.
At least that's to the best of my understanding; it's been a while since I have looked at any of this, so feel free to make corrections.
Isabelle is actually a "logical framework", so it supports intuitionistic logic, actually its meta theory is intuitionistic higher-order logic.
So this is not because of the logic, it is because of the mindset. Intuitionistic logic is usually championed by people who want to emphasise computation over reasoning, and that is why they build computation as one their reasoning steps into their kernel. They don't have to do that. They do it deliberately, because it aligns with what they like, and how they like to think about logic.
Pretty much. The kernel of a proof assistant is the absolutely trusted core, and ultimately gets to decide what is or isn't a proven mathematical fact (so roughly a kernel resource). Over that, you build a huge amount of (userspace) tooling that doesn't have to be absolutely trusted since its job is just to talk into the kernel and get theorems.
A kernel bug manifests as the kernel deciding that something is a theorem which shouldn't be. The worst case is when it decides that False is a theorem, from which it immediately follows that absolutely everything is a theorem.
As mentioned in the article, HOL Light gets away with a lot because it only cares about delivering theorems. Other systems want to retain the proofs as artifacts (sometimes called certificates), and once you do that, you need to make sure these artifacts aren't stupidly huge or otherwise useless. Provers such as Rocq (and I assume Lean) additionally want their proof objects to contain decent executable algorithms backing the proof.
HOL Light also does pretty much no evaluation. The most it understands of evaluation is that (λx. f) x = f. If you want to evaluate anything more complex than this, you build that in "userspace" and you do all the equational reasoning manually via the kernel.
Lean and Rocq kernels do full evaluation of recursive functions, so they have to come installed with an API for building those recursive functions and internal checking to make sure those functions are terminating. The article's author is asking whether you could redo something like Lean and Rocq where the recursive function API was much simpler. I've wondered for a while whether you could also have the evaluator as basic as HOL Light's, and do the rest in userspace. I think there were theorem provers like this that went out of fashion decades ago.
It used to be a much more exciting space before Lean somehow got everyone's attention. The author is the co-creator of Isabelle/HOL, and is still not sure why there is so much more excitement for Lean than for simple type theory.
In HOL Light? Just so you can run the proof objects through another prover like Isabelle. Wasn't that your original ambition?
As you know, Rocq and Lean folk want more than just that from their proof objects. They want proofs to contain executable code, often of the very programs they were verifying, and so treat their proof assistants like programming languages with verifiers attached. So you get complex recursion and inductive definitions baked into the kernel. Whether this is a good idea or not is obviously pretty disputed among us, though I'm mostly with you and Larry :)
> So you get complex recursion and inductive definitions baked into the kernel.
It is a pragmatic choice, just like a type system is. I think both of these choices are outdated now that formalisation is fast. What you really want is a simple semantics (what is the semantics of Lean again...?), and build on top of that by verified kernel extensions. Program extraction via proof objects doesn't really work, I don't think anyone does that for real. What you do is you write your program in your term language, and export the meaning of that term as a program. Isabelle does that, too, and you don't need proof objects for that.
In my current version of Practal (Practal Zero) I have a switch for keeping proof objects around as well, in case I want to maybe transform proofs in some reuse scenario. Not sure if I will actually use that, ever, because it would be slow, too. Also, I would rather prove that a certain transformation is correct, and then add this as a kernel extension.
> 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.
I mean it's an old term in algebra/analytics that predates sytem-kernels by 50 years or so. And even in the meaning compute/solver/gpu-kernel, even thuough predated by systems kernel, it has still been in use at least 30 years.
So proof kernel is not that far fetched, I think. I only skimmed the article though ... so not saying if it was good use here or not.
The one thing that gives me concern in their is "nanoda [the external proof checker] is [now] tracked daily". Although that would have caught this issue, we also now live in a world in which some model is going to think that hacking the proof-checker distribution is the obvious way to obtain the proof it is after; I expect that attempts on that will be much more common than soundness bugs. However, this is said without knowing what other measures are in place to assure the integrity of the distribution.
This used to be the bane of all machine learning experiments. It might have been lost to time but I once stumbled upon a big list of AI reward-hacks like this. Things like - we tried to develop fast cars, but the AI just made a really tall weighted stick that would fall over onto the finish line. And we tried to teach the AI not to lose in Tetris, so it hit pause whenever it was about to.
We have to remember that OpenAI wanted us to believe that an adversarial AI hacked Huggingface because it was "too ambitious".
Then an AI found a proof of False, hidden in the "proof" of the Collatz conjecture.
On the other hand we are supposed to believe that all Astra math results with no independent peer review are correct. The Lean proofs are tens of thousands of lines long with no comments where the main theorem even is.
The ambitious AI could have inserted another obfuscated proof of False or hidden False in the hypotheses of the main theorem, wherever that is.
Lean, due to its advanced features, has had the most of soundness bugs of all provers:
Essentially, it's just doing a lazy fixpoint a la Haskell's fix function. The definition is a little more general, though, to make it work for both transfinite and well-founded recursions as well.
The debate over proof objects versus proof types seems particularly ivory-tower, since it's all just data being processed by a computer. You invent this distinction between two kinds of things - "objects" and "types" - and then argue which one is better. No, I don't speak Lisp.
And you don't "throw away proofs" when using proof types. They are right there in the theory file if you want to check them again.
I have to admit that I know very little about formalized proofs, but the article seems to put some reasoning behind this distinction, specifically this statement:
> Because it is only the proof calculi that have proof objects that seemingly need to put everything into the kernel.
I interpret that to mean that for some reason, having proof objects requires or at least encourages putting more logic in the kernel (which is apparently equivalent to having more axioms) and that results in a greater risk of having bugs in the proof checker itself.
In every proof assistant something is doing all that logic, whether you call it a kernel or not.
As I understand their writing, ML is a language meant for developing proof assistants and this debate is specific to proof assistants written in ML, about the extent to which you use ML's type system as part of the kernel (proofs or theorems are types, at least partially), or write one yourself (proofs are just objects).
Even Rust has an unsound type system that allows arbitrary memory access in safe code, so you can't just assume your programming language has a sound type system.
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.
Ha, I actually wrote a paper pushing on this "kernel" pun between OSs and proof-checkers [1], designing a HOL kernel structured like an OS kernel.
[1]: https://drops.dagstuhl.de/storage/00lipics/lipics-vol269-typ...
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.
Yeah in theorem provers usually the opposite is true: "We want to put as little stuff as possible in the kernel because that's the part we need to verify by hand"
In an OS kernel that instinct is also true: 'we want to put as little as possible in the OS kernel, because that stuff can bring down the machine.'
That isn't true, as there are many things that can bring down the machine. If your X or Wayland server crashes, it brings down your machine.
No, that is true, even if not uniquely. A kernel bug can easily bring down the machine. Maybe Xorg can also manage it... although IMHO that also sounds like a kernel bug (surely it's the kernel's job to ensure no user program can do that?)... but that doesn't make the kernel safe. And I suspect it's easier to take down the machine from ring 0 than a display server even if both can do it.
It doesn't, it just loses your session
A kernel panic doesn't bring down the CPU, nor the hard drive, or the RAM, or the power supply unit. So if we're being pedantic, the machine is still up.
Well, a kernel bug gets write access to everything. A bug in userland is a bit more constrained in what it can do.
That counts especially for accidental bugs and denial of service. To make a userland bug exploited adversarially not impact the rest of the system requires more hardening of the kernel.
Yeah a userland bug just gets all my passwords, SSH keys, personal secrets and whatever.
Say it with me - there's no practical difference.
You are talking about a single user system.
You can compartmentalise further.
Modern processors even give you these 'rings' to help with the hardware side of that, if you want to.
Yes, these are the standard excuses. But has anyone actually thought about them in the last twenty years, in the context of the way we actually use computers?
Eh, yes? Just look the discussions surrounding the development of any web browser? Or look at the permissions system in Android or iOS or on Mac (and perhaps even Windows?).
So you acknowledge a browser bug is just as bad as a kernel bug.
A bug in the website itself is just as bad, if it's a website you care about.
They differ in how easy a fix is to develop and roll out, and what the blast radius is.
I think in the background of article's premises is an argument about classical vs. intuitionistic logic, rather than only about the merits of putting stuff in the kernel vs. outside.
Isabelle seems to use classical logic and set theory. Classical logic is often simpler, but when you do the "hard toil" (as the article puts it) of building recursive functions on set theory, all you've really done is to nonconstructively prove the existence of a set of pairs with certain properties. Good luck evaluating such an abstract "existence" with any concrete argument. Whereas intuitionistic logic as used by Coq is more complicated, but that's in part because its notion of "function" is an actual procedure in your computer that can accept an argument and produce a result.
At least that's to the best of my understanding; it's been a while since I have looked at any of this, so feel free to make corrections.
Isabelle is actually a "logical framework", so it supports intuitionistic logic, actually its meta theory is intuitionistic higher-order logic.
So this is not because of the logic, it is because of the mindset. Intuitionistic logic is usually championed by people who want to emphasise computation over reasoning, and that is why they build computation as one their reasoning steps into their kernel. They don't have to do that. They do it deliberately, because it aligns with what they like, and how they like to think about logic.
Pretty much. The kernel of a proof assistant is the absolutely trusted core, and ultimately gets to decide what is or isn't a proven mathematical fact (so roughly a kernel resource). Over that, you build a huge amount of (userspace) tooling that doesn't have to be absolutely trusted since its job is just to talk into the kernel and get theorems.
A kernel bug manifests as the kernel deciding that something is a theorem which shouldn't be. The worst case is when it decides that False is a theorem, from which it immediately follows that absolutely everything is a theorem.
The HOL Light kernel (mentioned in the article) is about 500 lines from one file (https://github.com/jrh13/hol-light/blob/master/fusion.ml), and is a very straightforward implementation of a simple type theory (https://en.wikipedia.org/wiki/HOL_Light#Logical_foundations). I'm not so familiar with Lean, but it would appear its kernel is spread over this C++ directory: https://github.com/leanprover/lean4/tree/master/src/kernel.
As mentioned in the article, HOL Light gets away with a lot because it only cares about delivering theorems. Other systems want to retain the proofs as artifacts (sometimes called certificates), and once you do that, you need to make sure these artifacts aren't stupidly huge or otherwise useless. Provers such as Rocq (and I assume Lean) additionally want their proof objects to contain decent executable algorithms backing the proof.
HOL Light also does pretty much no evaluation. The most it understands of evaluation is that (λx. f) x = f. If you want to evaluate anything more complex than this, you build that in "userspace" and you do all the equational reasoning manually via the kernel.
Lean and Rocq kernels do full evaluation of recursive functions, so they have to come installed with an API for building those recursive functions and internal checking to make sure those functions are terminating. The article's author is asking whether you could redo something like Lean and Rocq where the recursive function API was much simpler. I've wondered for a while whether you could also have the evaluator as basic as HOL Light's, and do the rest in userspace. I think there were theorem provers like this that went out of fashion decades ago.
It used to be a much more exciting space before Lean somehow got everyone's attention. The author is the co-creator of Isabelle/HOL, and is still not sure why there is so much more excitement for Lean than for simple type theory.
I added proof objects ages ago to HOL Light, it is not a big deal. It's just, as Larry said, why would you want them in the first place?
In HOL Light? Just so you can run the proof objects through another prover like Isabelle. Wasn't that your original ambition?
As you know, Rocq and Lean folk want more than just that from their proof objects. They want proofs to contain executable code, often of the very programs they were verifying, and so treat their proof assistants like programming languages with verifiers attached. So you get complex recursion and inductive definitions baked into the kernel. Whether this is a good idea or not is obviously pretty disputed among us, though I'm mostly with you and Larry :)
> So you get complex recursion and inductive definitions baked into the kernel.
It is a pragmatic choice, just like a type system is. I think both of these choices are outdated now that formalisation is fast. What you really want is a simple semantics (what is the semantics of Lean again...?), and build on top of that by verified kernel extensions. Program extraction via proof objects doesn't really work, I don't think anyone does that for real. What you do is you write your program in your term language, and export the meaning of that term as a program. Isabelle does that, too, and you don't need proof objects for that.
In my current version of Practal (Practal Zero) I have a switch for keeping proof objects around as well, in case I want to maybe transform proofs in some reuse scenario. Not sure if I will actually use that, ever, because it would be slow, too. Also, I would rather prove that a certain transformation is correct, and then add this as a kernel extension.
Hey, it's been awhile since we had a good microkernels vs monolithic debate. Time to post it!
> 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.
The word kernel always meant "the most important part of something".
Likewise "harness" can be used to mean "to collect and control something so that it can be used effectively".
As someone who spent years designing wiring harnesses for prototype and test vehicles, I am so tired.
I mean it's an old term in algebra/analytics that predates sytem-kernels by 50 years or so. And even in the meaning compute/solver/gpu-kernel, even thuough predated by systems kernel, it has still been in use at least 30 years.
So proof kernel is not that far fetched, I think. I only skimmed the article though ... so not saying if it was good use here or not.
Here is the postmortem of the lean bug: https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...
The one thing that gives me concern in their is "nanoda [the external proof checker] is [now] tracked daily". Although that would have caught this issue, we also now live in a world in which some model is going to think that hacking the proof-checker distribution is the obvious way to obtain the proof it is after; I expect that attempts on that will be much more common than soundness bugs. However, this is said without knowing what other measures are in place to assure the integrity of the distribution.
This used to be the bane of all machine learning experiments. It might have been lost to time but I once stumbled upon a big list of AI reward-hacks like this. Things like - we tried to develop fast cars, but the AI just made a really tall weighted stick that would fall over onto the finish line. And we tried to teach the AI not to lose in Tetris, so it hit pause whenever it was about to.
Was it this one? https://docs.google.com/spreadsheets/d/e/2PACX-1vRPiprOaC3Hs...
It's called reward hacking
https://en.wikipedia.org/wiki/Reward_hacking
We have to remember that OpenAI wanted us to believe that an adversarial AI hacked Huggingface because it was "too ambitious".
Then an AI found a proof of False, hidden in the "proof" of the Collatz conjecture.
On the other hand we are supposed to believe that all Astra math results with no independent peer review are correct. The Lean proofs are tens of thousands of lines long with no comments where the main theorem even is.
The ambitious AI could have inserted another obfuscated proof of False or hidden False in the hypotheses of the main theorem, wherever that is.
Lean, due to its advanced features, has had the most of soundness bugs of all provers:
https://cr.yp.to/proofs.html
The semiconductor industry uses ACL2 or HOL-light.
[dead]
The bigger the kernel gets, the more stuff you gotta hope is bug-free.
I'd rather keep it small and deal with the extra work somewhere else.
Intriguingly, Metamath handles recursive definitions by factoring out the recursion into a single higher-order function:
https://us.metamath.org/mpeuni/df-rdg.html
Essentially, it's just doing a lazy fixpoint a la Haskell's fix function. The definition is a little more general, though, to make it work for both transfinite and well-founded recursions as well.
This chashed out nicely in a sequence builder:
https://us.metamath.org/mpeuni/df-seq.html
which specializes to "normal" recursion.
Previous related discussion: https://news.ycombinator.com/item?id=49137060
The debate over proof objects versus proof types seems particularly ivory-tower, since it's all just data being processed by a computer. You invent this distinction between two kinds of things - "objects" and "types" - and then argue which one is better. No, I don't speak Lisp.
And you don't "throw away proofs" when using proof types. They are right there in the theory file if you want to check them again.
I have to admit that I know very little about formalized proofs, but the article seems to put some reasoning behind this distinction, specifically this statement:
> Because it is only the proof calculi that have proof objects that seemingly need to put everything into the kernel.
I interpret that to mean that for some reason, having proof objects requires or at least encourages putting more logic in the kernel (which is apparently equivalent to having more axioms) and that results in a greater risk of having bugs in the proof checker itself.
In every proof assistant something is doing all that logic, whether you call it a kernel or not.
As I understand their writing, ML is a language meant for developing proof assistants and this debate is specific to proof assistants written in ML, about the extent to which you use ML's type system as part of the kernel (proofs or theorems are types, at least partially), or write one yourself (proofs are just objects).
Even Rust has an unsound type system that allows arbitrary memory access in safe code, so you can't just assume your programming language has a sound type system.