3 ms·
Why is it all in the kernel?
- yjftsjthsd-h 3mo agoProof 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.
- eru 3mo agoYes, 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.
- lou1306 3mo agoYeah 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"
- eru 3mo agoIn 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.'
- inigyou 3mo agoThat 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.
- __s 3mo agoIt doesn't, it just loses your session
- inigyou 3mo agoA 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.
- eru 3mo agoWell, 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.
- inigyou 3mo agoYeah a userland bug just gets all my passwords, SSH keys, personal secrets and whatever. Say it with me - there's no practical difference.
- eru 3mo agoYou 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.
- inigyou 3mo agoYes, 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?
- 3mo ago
- wseqyrku 3mo ago> 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.
- voxelghost 3mo agoI 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.
- SkiFire13 3mo agoThe 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".
- myself248 3mo agoAs someone who spent years designing wiring harnesses for prototype and test vehicles, I am so tired.
- momentoftop 3mo agoPretty 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 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 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 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.
- practal 3mo agoI 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?
- codeflo 3mo agoI 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.
- practal 3mo agoIsabelle 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.
- dmulligan 3mo agoHa, 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-types2022/LIPIcs.TYPES.2022.1/LIPIcs.TYPES.2022.1.pdf https://drops.dagstuhl.de/storage/00lipics/lipics-vol269-typ...
- phendrenad2 3mo agoHey, it's been awhile since we had a good microkernels vs monolithic debate. Time to post it!
- red_trumpet 3mo agoHere is the postmortem of the lean bug: https://leodemoura.github.io/blog/2026-8-1-postmortem-for-kernel-soundness-bug-14576/ https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...
- ajb 3mo agoThe 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.
- inigyou 3mo agoThis 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.
- jubilanti 3mo agoIt's called reward hacking https://en.wikipedia.org/wiki/Reward_hacking https://en.wikipedia.org/wiki/Reward_hacking
- ameliaquining 3mo agoWas it this one? https://docs.google.com/spreadsheets/d/e/2PACX-1vRPiprOaC3HsCf5Tuum8bRfzYUiKLRqJmbOoC-32JorNdfyTiRRsR7Ea5eWtvsWzuxo8bjOxCG84dAg/pubhtml https://docs.google.com/spreadsheets/d/e/2PACX-1vRPiprOaC3Hs...
- monocasa 3mo agoPrevious related discussion: https://news.ycombinator.com/item?id=49137060 https://news.ycombinator.com/item?id=49137060
- deleted 3mo ago[deleted]
- xelxebar 3mo agoIntriguingly, Metamath handles recursive definitions by factoring out the recursion into a single higher-order function: https://us.metamath.org/mpeuni/df-rdg.html 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 https://us.metamath.org/mpeuni/df-seq.html which specializes to "normal" recursion.
- inigyou 3mo agoThe 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.
- brazzy 3mo agoI 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.
- inigyou 3mo agoIn 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.
- f12a8h 3mo agoWe 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 https://cr.yp.to/proofs.html The semiconductor industry uses ACL2 or HOL-light.
- glenstein 3mo ago[dead]
- cryptolobster 2mo agoThe 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.