You can't prove the hash function is correct, no. But you can prove the hash function is implemented equivalently to its definition. That's what the article is about.

That's true. But if you can't prove that your hash function has the desirable properties you expect/hope for, then I think that is important to acknowledge.

No, those are separate issues. There might be philosophical value on acknowledging the impossibility to prove the correctness of the algorithm, but it has little or no practical value when you want to prove if your implementation of the algorithm is correct.

Your argument is like saying that because there is no way to guarantee your physical product's design is 100% defect free, there is no point to implement quality controls in the manufacturing floor.

Does anyone want to write why they disagree instead of just downvoting me?

I'm not sure, but it seems like you're making a connection to P vs. NP that is at the least very non-obvious, so people default to thinking that you have no idea what you're talking about.

Maybe you could explain how proving a hash function correct implies P!=NP?

Sure thing. I'll write a blog post about it later tonight (am on work time right now)

Brief summary however: The point of a crypto hash function is that you need to try on the order of 2^n inputs (n being length in bits of digest) to find a collision. (greater than polynomial time) However you can check any input in polynomial time. This makes it in NP. (decision problem is computable in polynomial time). I'm probably missing some details which I will think about later :)

Watch Dan Boneh's coursera cryptography course where he at least mentions that provably secure cipher systems require that P != NP. Combine that with the wikipedia article on cryptographic hash functions which tells you that you can build ciphers from hash functions. Done.

O(2^(n/2)) actually, due to the birthday attack.

I did not downvote you. However, can you explain your statement "You can't prove a cryptographic hash function is correct without proving P != NP."