3 ms·

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

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.

random314 6y ago
It would be interesting if you can show how Coq refused to accept the old formula and what error it produced.
- gopiandcode 6y ago
  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/70927c5b50e21a08f510cfd9555d8324a61c1233 https://github.com/certichain/ceramist/commit/70927c5b50e21a...
- jhanschoo 6y ago
  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.
ImaCake 6y ago
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 :)
sukilot 6y ago
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.
- gopiandcode 6y ago
  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.
karmakaze 6y ago
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.

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.

random314 6y ago

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

gopiandcode 6y ago
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/70927c5b50e21a08f510cfd9555d8324a61c1233 https://github.com/certichain/ceramist/commit/70927c5b50e21a...
jhanschoo 6y ago
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.

ImaCake 6y ago

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 :)

sukilot 6y ago

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.

gopiandcode 6y ago
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.

karmakaze 6y ago

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.