Hacker News Reader

Comment by bawolff | Hacker News Reader

This is important work and all, but i can't help but feel the headline is a bit clickbaity

The headline and the entire intro are clickbaity. While this is interesting from a theoretical math perspective, it is completely irrelevant in practical use of bloom filters. Typical filters will have a much larger number of bits than the number of hash functions used, making the probability of overlapping bits vanishingly small, and thus the original wrong calculation is a perfectly fine approximation.

So none of this matters for malicious site filters, or anything like that. And the reason why it took 30 years to notice the original problem is that, if you just test the false positive rate for typical Bloom filters empirically, you'd come within error margins of the "wrong" result anyway. It's not like people trusted critically bad math for 30 years. The bad math was formally speaking wrong, but close enough to the right result for nobody to notice nor care.

I know mathematicians have to sell their research, but sorry, with this one you didn't advance the state of the art of practical Bloom filter usage, just the state of the art of formal proofs :-)

For Bloom filters specifically I preferred last year's "On Occupancy Moments and Bloom Filter Efficiency". You wouldn't guess from the title or abstract, but it's fairly comprehensive, including proofs of the expected false positive rates.

https://arxiv.org/abs/1908.04810

I don't know enough about bloom filters or the math involved to say whether or not you are correct.

But what you're saying sounds a lot like many proponents of various flavors of NoSQL, Eventual Consistency, etc. I.e., it sounds like you are saying that lots of people have been using it for a long time, and it's just good enough. The actual correctness isn't really that big a deal.

I might be crossing domain boundaries here and thinking up stuff that really doesn't matter. I mean, bloom filters have a known challenge. No one was ever supposed to use them except for statistical purposes anyway, and with a known error rate, it's fine to add into your models.

But there's also something that feels a little weird about your point. It sounds like you're saying it's good enough for X, Y, and Z use cases; therefore it doesn't really matter how technically wrong it is.

But again, I could be really off.

Your comparison isn't really appropriate. Bloom filters work, they worked before this proof and they work the same way after the proof. This result isn't about how correct Bloom filters are or aren't. Their caveats are understood, and even using the "bad" math from the original paper, their performance in practical scenarios could be estimated with enough accuracy to use them in practical applications. I dare say not a single user of bloom filters will change anything about their implementation stemming from this result.

For example, if you size a bloom filter a certain way, the "bad" math might tell you your false positive rate is 0.001%, while the "good" math might tell you your false positive rate is 0.001002%. It makes no difference. The error is orders of magnitude smaller than the number you get anyway. (I made those numbers up, but I've used Bloom filters and they should be in the ballpark for the sizes I've worked with). The bad math might be strictly speaking incorrect, but it's a good enough approximation for all practical purposes.

This is different from Eventual Consistency stuff, which has real practical implications from not having certain guarantees. Those limitations are real, and they have real consequences, not just a rounding error in a number.

The difference between approximate and exact false positive rate calculations in real-world scenarios is insignificant. It's fine to use the approximation.

If you had very specific tolerances here you wouldn't work in terms of the expected false positive rate anyway; you'd build your filter and validate on the real thing.

A footnote in the article notes that the original "faulty" formula and the new "correct" one are asymptotically equivalent.

Yes, that's a fair comment. I took some creative liberties with the title to try and make this theoretical result more relatable to the average reader, but it's possible I may have gone too far.

You went too far. Your title is wrong in the same way your research shows bloom filters are wrong. You chose relatable over correct. By gettnig the obvious stuff wrong right at the top, you shatter reader's trust that you got the non obvious stuff right.

Thanks for the feedback - I figured presenting the exact Coq proofs directly would probably be too dry, and thus was trying to give some context for the work to make the presentation more interesting. In hindsight, I can see how this has been detrimental to some other parts of the article.

If you look at the related work section of the paper, we actually present a multitude of papers in the literature (even some recent as 2019) that actually still incorrectly refer to Bloom's expression as an exact bound, so I thought at the time that the "debunking" title was not inaccurate.

I'll keep your advice in mind the next time I write an article about research work.

Yes absolutely too far: clickbait and that's unfortunate because it otherwise looks like a really well written article. It completely ignores all the work that happened in those 30 years before this Coq proof which only replicates (with more trustable steps) other work.

As someone totally unaware of bloom filters, I appreciate the click bait title because it made me aware of them, and then almost immediately understand what they are thanks to the clear explanation and visuals :)

It would be interesting if you can show how Coq refused to accept the old formula and what error it produced.

When I was attempting to prove Bloom's original incorrect bound, the work never progressed to the point where I was actively working directly on proving his bound - I managed to prove some intermediate theorems, but was unable to work out a way to compose them. The issue ended up being that that I was unable to derive the independence required to prove the inductive step.

If you're interested at looking at the sources, I think the following commit was around the place where I was working on this: https://github.com/certichain/ceramist/commit/70927c5b50e21a...

Note that you don't really "get <a proof assistant> to refuse to accept" an incorrect result, you just fail to construct a proof for it, as the author talks about in their reply.

What you can do, sometimes, is succeed in proving the negation of the incorrect result.

Yes and it’s even worse than most clickbait, because the way it accomplishes its attention grab is to misleadingly throw shade on bloom filters themselves, which the content in no way justifies. Leaves me feeling a little sick to my stomach. Ugh.

Then again, HN doesn't auto-collect, it's all user-submitted, which makes "click bait" basically irrelevant: a real user though this was worth sharing, and enough folks agreed to get it on the front page?

'Clickbait' can still be submitted by real users and upvoted, though. If the title is a tease that forces you to click on the link to resolve it, it's clickbait.

Reply on news.ycombinator.com