12 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 3mo 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 3mo agoThe implementation of the kernel is relatively trivial, it's an intentional design choice.
- sieabahlpark 3mo ago[dead]
- Cantinflas 3mo 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 3mo agobut where’s the seam!?
- deleted 3mo ago[deleted]
- why_only_15 3mo 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 3mo 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 3mo ago> much simpler type checkers like Rust's Linear/Affine types aren't easy, although deep down it is about enforcing XOR.