Re: On raw strings in <origin> commit field

[Liliana Marie Prikler <liliana.prikler@gmail.com>]

Am Mittwoch, dem 05.01.2022 um 04:28 -0500 schrieb Mark H Weaver:
> Hi Liliana,
> 
> Earlier, I wrote:
> > Sorry, but this is not even close to a valid argument that the set
> > of possible push actions to a Git repo is uncountable.  In fact,
> > it's quite easy to prove that the set is countable.  Any
> > mathematician will know this.
> 
> I suppose I should give a proof.  I'll give two proofs.
Now, those two proofs are nice and I'm not going to dispute them. 
However, just for the record I do think that you're paying a little too
much attention to formalisms and too little to everything else I'm
saying.  In the case of Cantor vs. the liar paradox (which I've wrongly
attributed to Cantor because his proof is being used in Gödel's
incompleteness theorem and the Halting Problem¹), that's completely on
me, although I'm not sure whether that suffices for gaslighting.  In
any case, it was not intentional.  In this context, on the other hand,
it ought to have been comparatively easy to infer that I was talking
about push actions (plural) as sequences, not as individual push
actions like you've used for your proof.

From here on, I will assume that each individual push action is finite
as you did, but I don't think that using communications of finite
length are a helpful building block here.  Porting Git to Turing
Machines would have the effect of allowing an infinite tape shared
between multiple machines and they could possibly run forever. 
However, I am going to assume that each individual push action is
finite anyway, as your assumptions will typically hold for reasons of
practicability.  Note, though, that this would not suffice for
robustness arguments.  Whatever communications you make at a given
time, you can not be sure that your observations will be replicated if
you repeat them (even if restricted to fetching only).

As we're trying to generalize your proof for a single push action to be
chosen among a finite set to all communications to a series of push
actions, we do encounter a problem if we were to encode this as a mere
list of push actions.  This can be done by a rather simple Cantor
proof:  The set of lists of a particular type T which admits at least
two values is uncountable (a list of booleans can be directly mapped to
a binary number and thus Cantor's original proof applied).  Since there
are more than two permissible push actions, we have a problem.

Luckily, there is a straightforward solution.  A push action can only
create new commits (of which there are finitely many, both in terms of
the content committed as per your argument as in their count by the
limited number of SHA-1 hashes), create new branches (which must have a
finitely long name as per your argument), or create tags (which also
must have finitely long names, again per your argument).  There are no
other operations worth mentioning and a push action must contain at
least one action to be valid.  Therefore, a valid sequence of push
actions is finite, as it will inevitably end up using all SHA-1 hashes
as well as all possible branch and tag names in some configuration. 
Q.E.D.

Remember the ¹ I wrote earlier?  Now originally, I had planned to write
a formal proof to show how validating a tag (i.e. making sure it does
not get assigned to a different commit) and likewise validating a
commit after SHA-whateverthenextattackwillbenamed would be co-RE-hard.
It would likely have invoked Cantor at some point, though again perhaps
at a lower level than you'd have liked.  But I am sure you agree, that
this proof that Git is completely safe, actually, is much nicer.  There
shouldn't be anything that could discredit it, least of all something
past me would have said.  WDYT?