Comment by gr_norm
1 day ago
> The practical consequence: checking with an independent kernel still works, since it required two distinct bugs in two implementations, but users who rely on it need current versions of both.
Things like this aren't too surprising, given that even much simpler type checkers like Rust's have soundness issues occasionally. I think it's very important to view verified results not as an absolute and unbreakable guarantee, just an extraordinarily strong one where (1) the surface area for soundness issues has been painstakingly minimized and (2) any realized soundness issues are taken very seriously and fixed in short order.
The implementation of the kernel is relatively trivial, it's an intentional design choice.
As claude would say, "relatively" is carrying a lot of weight in that frase. Definitely load-bearing — would not pass a quick smoke test.
but where’s the seam!?
[dead]
> much simpler type checkers like Rust's
Linear/Affine types aren't easy, although deep down it is about enforcing XOR.
To what degree can you say something like "if the kernel doesn't have metaprogramming [or some other set of features] it's fine". When were the last bugs with a reduced feature set?
Read the article. The elaborator (where metaprogramming is evaluated) is not part of the trusted computing base. The security model is that bad proof terms get rejected, not that they're never generated.