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

Postmortem for Kernel Soundness Bug #14576

leodemoura.github.io

Post reply on HN
Print view View original

61–68 of 68 posts

Re: Postmortem for Kernel Soundness Bug #14576

#61

Post by jojomodding »

senderista wrote: post #56
alethic wrote: post #54

Earlier quoted context omitted.

The utility of autoformalization is not actually in confirming the correctness of human-checked results. Mathematicians have a pretty good peer review process. I'm not actually aware offhand of any mathematical results that were accepted and later found to be incorrect -- though I'm sure cases exist, it's astoundingly rare. The mathematics community's motivation for formalizing problems like Maryna Viazovska's sphere…

> I'm not actually aware offhand of any mathematical results that were accepted and later found to be incorrect https://mathoverflow.net/questions/35468/widely-accepted-mat...

Yes, in particular the slides by Kevin Buzzard (linked in there or here: https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/sli... ) are funny and educational on that matter.

Re: Postmortem for Kernel Soundness Bug #14576

#64

Post by stevefan1999 »

gr_norm wrote: post #5

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

> much simpler type checkers like Rust's

Linear/Affine types aren't easy, although deep down it is about enforcing XOR.

Re: Postmortem for Kernel Soundness Bug #14576

#65

Post by cyphar »

j16sdiz wrote: post #51
chowells wrote: post #50

Earlier quoted context omitted.

That's not what it says. It says that as long as the logic is rich enough (first-order isn't enough) and consistent there are statements where neither the statement nor its negation is provable. You may choose to create a new logic by adding either the statement or its negation as an additional axiom, and it will (obviously?) remain consistent. Truth is some sort of value judgment that is outside the scope of formal…

err... There are always more ---> you can't make it "compete" by adding finite number of axioms

You can make it complete, it just won't be consistent.

In fact there is a simple way to do it -- add contradictory axioms and then you can use the principle of explosion to prove any statement as true. Is such a system inconsistent and thus useless? Yes, but it is complete.

Re: Postmortem for Kernel Soundness Bug #14576

#66

Post by esterna »

why_only_15 wrote: post #46
gr_norm wrote: post #5

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

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.

Re: Postmortem for Kernel Soundness Bug #14576

#67

Post by xelxebar »

i2talics wrote: post #44
xelxebar wrote: post #34

Earlier quoted context omitted.

That's with the original C verifier only. The actual database is cross-checked by 6 independent implementations. This is the whole point of Metamath: its kernel is so tiny that you can implement a verifier in a weekend. Metamath isn't a silver bullet in the design space of formal proof tools, but I personally think it just about nails the metatheory we want. Maybe some explicit facility around definitions would be de…

Why does the original C verifier have bugs if its supposedly so easy to implement a verifier?

Ease of implementation means we get more, independent verifiers rather than trusting any particular one.

Re: Postmortem for Kernel Soundness Bug #14576

#68

Post by alethic »

alethic wrote: post #54
michaelfm1211 wrote: post #18

Reminds me of this: https://mathoverflow.net/questions/513742/are-we-stuck-with-... I know this is an implementation bug not a meta-theory bug, but I'd almost consider the fact soundness bugs are possible as a bug in the ideology, or at least a severe drawback. Stuff like this just wouldn't happen in Metamath. In a future where AI is autogenerating formalizations, why not have the AI use a harder but airtight system…

The utility of autoformalization is not actually in confirming the correctness of human-checked results. Mathematicians have a pretty good peer review process. I'm not actually aware offhand of any mathematical results that were accepted and later found to be incorrect -- though I'm sure cases exist, it's astoundingly rare. The mathematics community's motivation for formalizing problems like Maryna Viazovska's sphere…

(I should note that there is also utility in confirming the correctness of results that are too complex to be adequately verified by humans. The recent result that NF is consistent wrt. ZFC, among others (Peter Scholze's Liquid Tensors project) are examples of this. But that's distinct from "autoformalization" as commonly applied.)
Post reply on HN