4 ms·
I wonder if hashes are discouraged at JPL due to a historical focus on "correct, and provably correct" code. Hash collisions happen. Yes, you can make collisio
by dmurray 5y ago
I wonder if hashes are discouraged at JPL due to a historical focus on "correct, and provably correct" code. Hash collisions happen.
Yes, you can make collisions arbitrarily unlikely, and there are so many situations where they come in useful, but I can imagine an engineering culture where they are just never an easy tool to reach for.
- dnautics 5y agoYou can axiomatize uniqueness of hashes in proof systems.
- ethbr0 5y agoThis would require a hash input (or combination of inputs) to be unique over a limited / expected domain, right?
- ncallaway 5y agoI mean, you could take anything as an axiom so there are no real requirements for it. I would imagine you would want to demonstrate the P(collision|domain+operating lifetime) << acceptable level or risk, and after you’d done that, take the uniqueness of hashes as a axiom for the proof system? That’s just speculation on my part, since I haven’t done much with formal proofs of working code
- dnautics 5y agoNo you just special case the function call and tell the proof analyzer "this never happens". Strictly speaking, a lie, but probably a sophisticated prover could even be rigged to keep track of those conditions (not in x years, e.g.) if you so chose
- SV_BubbleTime 5y ago> arbitrarily unlikely IDK, I would call more possibilities than grains of sand in the universe a little more than “arbitrarily unlikely”.