Date: Fri, 18 Feb 2022 07:34:52 +0000
To: "David A. Harding" <dave@dtrt.org>,
 Bitcoin Protocol Discussion <bitcoin-dev@lists.linuxfoundation.org>
From: ZmnSCPxj <ZmnSCPxj@protonmail.com>
Reply-To: ZmnSCPxj <ZmnSCPxj@protonmail.com>
Message-ID: <8RVJuPI1U7Iw74uWuGwQyJIvJYBWzJM9RJZKNy_KXAMaFJP9uHmAaq8UOCJ2jxiM6n1CvyYrUXZ0TUWOPoZ5Ja6oCtLsf62qhS7aN_vkZMw=@protonmail.com>
In-Reply-To: <0100017ee6472e02-037d355d-4c16-43b0-81d2-4a82b580ba99-000000@email.amazonses.com>
References: <CAMZUoK=pkZuovtifBzdqhoyegzG+9hRTFEc7fG9nZPDK4KbU3w@mail.gmail.com>
 <87leymuiu8.fsf@rustcorp.com.au>
 <CAD5xwhgP2_51Dvar0f1tsMrCXZ61W9-HnLgR45D-54Oc7-X1ag@mail.gmail.com>
 <0100017ee6472e02-037d355d-4c16-43b0-81d2-4a82b580ba99-000000@email.amazonses.com>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: quoted-printable
Subject: Re: [bitcoin-dev] Recursive covenant opposition,
	or the absence thereof,
	was Re: TXHASH + CHECKSIGFROMSTACKVERIFY in lieu of CTV and
	ANYPREVOUT
Precedence: list

Good morning Dave,

> On Mon, Feb 07, 2022 at 08:34:30PM -0800, Jeremy Rubin via bitcoin-dev wr=
ote:
>
> > Whether [recursive covenants] is an issue or not precluding this sort
> > of design or not, I defer to others.
>
> For reference, I believe the last time the merits of allowing recursive
> covenants was discussed at length on this list[1], not a single person
> replied to say that they were opposed to the idea.
>
> I would like to suggest that anyone opposed to recursive covenants speak
> for themselves (if any intelligent such people exist). Citing the risk
> of recursive covenants without presenting a credible argument for the
> source of that risk feels to me like (at best) stop energy[2] and (at
> worst) FUD.

Let me try to give that a shot.

(Just to be clear, I am not an artificial intelligence, thus, I am not an "=
intelligent such people".)

The objection here is that recursion can admit partial (i.e. Turing-complet=
e) computation.
Turing-completeness implies that the halting problem cannot be solved for a=
rbitrary programs in the language.

Now, a counter-argument to that is that rather than using arbitrary program=
s, we should just construct programs from provably-terminating components.
Thus, even though the language may admit arbitrary programs that cannot pro=
vably terminate, "wise" people will just focus on using that subset of the =
language, and programming styles within the language, which have proofs of =
termination.
Or in other words: people can just avoid accepting coin that is encumbered =
with a SCRIPT that is not trivially shown to be non-recursive.

The counter-counter-argument is that it leaves such validation to the user,=
 and we should really create automation (i.e. lower-level non-sentient prog=
rams) to perform that validation on behalf of the user.
***OR*** we could just design our language so that such things are outright=
 rejected by the language as a semantic error, of the same type as `for (in=
t x =3D 0; x =3D y; x++);` is a semantic error that most modern C compilers=
 will reject if given `-Wall -Werror`.


Yes, we want users to have freedom to shoot themselves in the feet, but we =
also want, when it is our turn to be the users, to keep walking with two fe=
et as long as we can.

And yes, you could instead build a *separate* tool that checks if your SCRI=
PT can be proven to be non-recursive, and let the recursive construct remai=
n in the interpreter and just require users who don't want their feet shot =
to use the separate tool.
That is certainly a valid alternate approach.
It is certainly valid to argue as well, that if a possibly-recursive constr=
uct is used, and you cannot find a proof-of-non-recursion, you should avoid=
 coins encumbered with that SCRIPT (which is just a heuristic that approxim=
ate a tool for proof-of-non-recursion).

On the other hand, if we have the ability to identify SCRIPTs that have som=
e proof-of-non-recursion, why is such a tool not built into the interpreter=
 itself (in the form of operations that are provably non-recursive), why ha=
ve a separate tool that people might be too lazy to actually use?


Regards,
ZmnSCPxj