Gopiandcode > logs > Bloom filters debunked: Dispelling 30 Years of bad math with Coq!
Bloom filters debunked: Dispelling 30 Years of bad math with Coq! July 23 2020 #projects #research #coq #verification Introduction There's this rather nifty feature of modern web browsers (such as Firefox or Chrome) where the browser will automatically warn the user if they happen to navigate to a "...
Hasnain says:
Very interesting read on data structures, proofs, and the history of Bloom filters. There is now a machine verifiable proof of the false positive rate of these things!
I also appreciated the explanation - it's one of the clearest explanations of bloom filters I've seen.
"In fact, as it turns out, the behaviours of a Bloom filter have actually been the subject of 30 years of mathematical contention, requiring multiple corrections and even corrections of these corrections.
Given this history of errors, can we really have any certainty in our understanding of a Bloom filter at all?
Well, never fear, I am writing this post to inform you that we have just recently used Coq to produce the very first certified proof of the false positive rate of a Bloom filter, finally putting an end to this saga of errors and returning certainty (pardon the pun1) to a mechanism that countless people rely on every single day."
(the site is not deceptive, it's sharing a screenshot of that dialog)
Posted on 2020-07-25T20:11:18+0000