5 ms·
> The practical consequence: checking with an independent kernel still works, since it required two distinct bugs in two implementations, but users who rely on
by gr_norm 2mo 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.
- rzmmm 2mo agoThe implementation of the kernel is relatively trivial, it's an intentional design choice.
- sieabahlpark 2mo ago[dead]
- Cantinflas 2mo agoAs claude would say, "relatively" is carrying a lot of weight in that frase. Definitely load-bearing — would not pass a quick smoke test.
- UqWBcuFx6NV4r 2mo agobut where’s the seam!?
- deleted 2mo ago[deleted]
- why_only_15 2mo agoTo 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?
- esterna 2mo agoRead 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.
- stevefan1999 2mo ago> much simpler type checkers like Rust's Linear/Affine types aren't easy, although deep down it is about enforcing XOR.