[Cryptography] LUKS on ATA versus on SSD
Ron Garret
ron at flownet.com
Sun Jan 4 12:26:15 EST 2026
> On Jan 3, 2026, at 5:17 PM, Jon Callas <jon at callas.org> wrote:
>
> The point of Godel numbering is that you take a set of symbols and properties and you can perform operations with them to assemble them
No, the point of Godel numbering is that it allows you to map strings of symbols onto NUMBERS, and then you can manipulate those numbers using mathematical operations like addition and subtraction in ways that correspond to symbolic operations, such as the ones you perform when constructing formal proofs. And that, in turn, allows you to prove some interesting negative results about formal proofs of claims about numbers. None of that has anything to do with block devices or hash functions.
> Godel's proof lets you iterate an infinite number of times
That's a red herring. The construction of Godel numbers is completely independent of Godel's proof. They actually have nothing to do with his proof except as a historical accident. To carry out Godel's proof you need some mapping from strings of symbols to numbers. Such a thing didn't exist in 1931 so Godel invented one. But the mapping he invented is an incredibly bad design relative to what came later and there is absolutely no reason to give Godel numbers any consideration today except as an item of historical interest and academic precedence. Godel numbers are as relevant today as Thomas Savery's steam engine.
> if you have finite symbols and finite iteration, then you can construct some mapping that looks like a hash function if you squint at it the right way
Yes, of course you can. You can always reduce anything to a Turing machine or one of its many equivalents. You could even invent a Godel machine based on Godel numbers that was Turing equivalent [1]. But there's a reason no one does this. Likewise, you can (if you squint hard enough and put on some really thick glasses) construct an analogy between block devices and Godel numbers, and you can even make that mapping look like a hash function. But again, there is a reason no one does this, and suggesting to someone trying to learn that this might be worthwhile does them a serious disservice.
> If Douglas finds it useful as an analogy to help understand the other problem, it seems like a quibble to say that well, it's only Godel numbering if the disk has infinite storage. Consider some suitable finite subset of the general problem, like strings that are less than 2^1,000,000 bits long. We (probably) can't represent strings longer than that in our material world anyway.
It's not about being finite vs infinite, it's about whether or not Godel numbering is a good analogy to the block device abstraction, and it isn't. Don't forget Douglas's original question:
> Is that -- block device can be anything that implements a block device -- because of how Turing machines / Godel numbering work, basically?
That answer to that is an emphatic NO. Block devices have nothing to do with Godel numbering, and they have nothing to do with Turing machines (except insofar as everything in computer science has to do with Turing machines, and Godel numbering is a Turing-complete abstraction). Block devices are nothing more than an abstraction of different kinds of hardware that makes them look as if they were the same kind of hardware. That's it.
rg
---
[1] In fact, building a Turing-complete "Godel machine" is pretty much what Godel did in his original proof, though of course he did not and could not have realized this as Turing's paper was still five years in the future.
More information about the cryptography
mailing list