[geofft]

> As one of the developers of this patchset, can you comment on how these contributions will be licensed?

Yes, I can comment on this. The licensing is the same as any other submission to the Linux kernel. See https://www.kernel.org/doc/html/latest/process/license-rules... for Linux kernel licensing in general and also https://www.kernel.org/doc/html/latest/process/submitting-pa... for the meaning of the Signed-off-by lines.

> Can you also comment on how a third party can verify or audit the output of a compiler without a specification?

I imagine it's pretty similar to how you verify or audit the output of a compiler with a specification. If you can show me an example of the sort of verification or audit you envision, I can perhaps give you a more helpful comment.

We do not make any claims about verified or audited compiler outputs or compliance with specifications, and to the best of my knowledge, the Linux kernel does not currently verify or audit any compiler outputs, so I'm not sure I follow why I would be particularly qualified to comment on it, but I could maybe point you at some interesting research.

> Can you comment on what empirical evidence you based this statement on?

Yes, I did comment on this, in the paragraph you quoted. If you'd like me to expand on something can you clarify?

[grumblenum]

>I imagine it's pretty similar to how you verify or audit the output of a compiler with a specification.

I must be missing the humor here. You can test against a specification to verify implementation. Testing an implementation against itself is meaningless. I would think that this is obvious. Also I don't typically use the word "empirical" to indicate purely qualitative assessments or intuition. You also provided a dead link.

[geofft]

Fixed the link, thanks.

There's no attempt at humor here - I'm just trying to get you to explain what, precisely, you mean by "test against a specification to verify implementation" so that we're in agreement on terms.

When I hear "test against a specification" and "verify implementation," I think about things like CompCert. But the Linux kernel does not use CompCert, it uses GCC or Clang. To the best of my knowledge, neither is tested against a specification and neither has a verified implementation.

Actually, when we first started discussing mainlining this, we had a bit of discussion about whether it was safe to allow rustc-compiled Rust code to link against GCC-compled C code. The specific worry was potential compiler bugs, of which the kernel has historically run into many. We eventually decided the risk was low, but the kernel has gone through periods where it insisted you use the exact same compiler for the kernel and for modules because of bugs. Those bugs have gone away through the normal human process of writing better code, not through formal verification. And when they existed, the kernel's response was not to reject those compilers, it was to work around the bugs.

Also, CompCert does not test against the C standard, which is written in English prose. It tests against the CompCert developers' attempt to re-express the C standard in terms of machine-checkable theorems. The C standard is confusing even to human readers, so it would be misleading to say that CompCert has verified their compiler against the standard as published by the standards committee. (Hence my claim that they're similar; you can verify a compiler of any language provided you write your own machine-checkable statements about what you expect it to do, and you still need other humans to read those theorems and convince themselves that they're the right ones.)

For those reasons, I'm trying to understand what your question is in a precise manner. Are you asking about things like CompCert? Because if so, I don't follow the relevance to our work, though again, I'm happy to point you at interesting research.

[grumblenum]

Just FYI, I didn’t read any of that wall, but it did make me laugh that you wrote it. You should go tell your rest friends to check the slack and down vote.