Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Why is it all in the kernel?

lawrencecpaulson.github.io

Post reply on HN
Print view View original

11–20 of 43 posts

Re: Why is it all in the kernel?

#11

Post by momentoftop »

practal wrote: post #8
momentoftop wrote: post #7

Earlier quoted context omitted.

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 theore…

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 :)

Re: Why is it all in the kernel?

#12

Post by practal »

momentoftop wrote: post #11
practal wrote: post #8

Earlier quoted context omitted.

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 a…

> 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.

Re: Why is it all in the kernel?

#14

Post by lou1306 »

eru wrote: post #4
yjftsjthsd-h wrote: post #2

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"

Re: Why is it all in the kernel?

#15

Post by SkiFire13 »

wseqyrku wrote: post #6
yjftsjthsd-h wrote: post #2

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.

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".

Re: Why is it all in the kernel?

#16

Post by practal »

codeflo wrote: post #10
yjftsjthsd-h wrote: post #2

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.

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 nonconstructivel…

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.

Re: Why is it all in the kernel?

#17

Post by ajb »

red_trumpet wrote: post #3

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.

Re: Why is it all in the kernel?

#18

Post by eru »

lou1306 wrote: post #14
eru wrote: post #4

Earlier quoted context omitted.

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.'

Re: Why is it all in the kernel?

#19

Post by xelxebar »

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.

Re: Why is it all in the kernel?

#20

Post by inigyou »

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.

Post reply on HN