Date: Fri, 16 Apr 2021 14:35:31 +0000
To: Jeremy <jlrubin@mit.edu>,
 Bitcoin Protocol Discussion <bitcoin-dev@lists.linuxfoundation.org>
From: ZmnSCPxj <ZmnSCPxj@protonmail.com>
Reply-To: ZmnSCPxj <ZmnSCPxj@protonmail.com>
Message-ID: <9jIB9EQTV4UY5OieVmn5P791NA3Oq3WJ2EXaG0fqscLxQx913zD6ds46YHXAie9JvKuZ0CpiRUUiXjHuosfyuzFdlQhgOUeiolZaca8_zQA=@protonmail.com>
In-Reply-To: <CAD5xwhiwYLe8-0Ya2msJY5+XrTERCS20epALpqUPXz-0FEKZTg@mail.gmail.com>
References: <CAD5xwhiwYLe8-0Ya2msJY5+XrTERCS20epALpqUPXz-0FEKZTg@mail.gmail.com>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: quoted-printable
Subject: Re: [bitcoin-dev] Designing Bitcoin Smart Contracts with Sapio
	(available on Mainnet today)
Precedence: list

Good morning Jeremy, et al.,


> Bitcoin Developers,
>
> I'm very excited to introduce Sapio[0] formally to you all.

This seems quite interesting to me as well!

I broadly agree with the rant on monetary units.
In C-Lightning we always (except for some legacy fields that will eventuall=
y be removed) output values as strings with an explicit `msat` unit, even f=
or onchain values (the smallest of which are satoshi, but for consistency w=
e always print as millisatoshi), and accept explicit `btc`, `sat`, and `msa=
t` units.

--

Personally I would have used a non-embedded DSL.

In practice an embedded DSL requires a user to learn two languages --- the =
hosting language and the embedded language.
Whereas if you designed a non-embedded DSL, a new user would have to learn =
only one language.
For instance, if an error is emitted, then the user has to know whether the=
 error comes from the hosting language compiler, or the embedded language i=
mplementation.

In a past career embedded DSLs for hardware description languages were bein=
g pushed, and we found that one of the drawbacks was the need to learn as w=
ell the hosting language --- at some point Haskell-embedded DSLs became so =
unpopular that anything that was even Haskell-related had a negative reacti=
on in some hardware design shops.
For example BlueSpec originally was a Haskell-embedded DSL, and eventually =
implemented a Verilog-like syntax that was not embedded in Haskell, becomin=
g BlueSpecSystemVerilog.

Further, as per coding theory, the hosting language is often quite generic =
and can talk about anything, including other embedded languages, thus we ex=
pect (all other things being equal) that in general, an utterance in an emb=
edded DSL will be longer than an utterance in a non-embedded DSL (as there =
is more things to talk about, more symbols are necessary, and thus we expec=
t things to be longer in the generic hosting language).
Whereas a non-embedded DSL can cut away most of the extra verbage needed to=
 introduce to the hosting language implementation, in order to indicate the=
 "entry" into the domain-specific language.

--

If my understanding is correct, I seem, that the hosting language is a full=
, general, Turing-complete language, that "builds up" a total (non-Turing-c=
omplete) contract description.

I have had (private) speculations before that it would be possible to desig=
n a language with two layers:

* A non-Turing-complete total "base language".
* A syntax meta-language similar to Scheme `syntax-rules`, which constructs=
 ASTs for the "base language".

Note that Scheme `syntax-rules` is indeed Turing-complete, as a macro can e=
xpand to a form with two lists that form two "ends" of a tape, and act as a=
 Turing machine on that tape, thus Turing-equivalent.
It is not a general language as it lacks many basic practicalities, but as =
pure computation, indeed it is possible to compute anything in that languag=
e.

The advantage of this scheme is that the meta-language is executed at langu=
age compile time, and the developer can see (by observing the compilation p=
rocess) whether the meta-program halts or not.
However, the end-user executing the program is assured that the program, de=
livered as a compiled binary, will indeed terminate, as the base language i=
s total and non-Turing-complete (i.e. the halting problem is trivial for th=
e base language --- all programs halt).

I even have started designing a syntax scheme that adds in infix notation a=
nd indent-sensitivity to a Lisp-like syntax, at the cost of disallowing typ=
ical Lisp-like names like `pair?`, e.g.

    foo x =3D value (bar x)
      where
        bar x =3D x

is equivalent to:

    (`=3D` (foo x)
         (value (bar x)
                (where
                  (`=3D` (bar x) x))))

I can provide more details if interested.

Note that the base language is not embedded in the meta-language, as the me=
ta-language is effectively only capable of talking about how the utterance =
in the base language is constructed --- the meta-language is not quite gene=
ral enough (i.e. the meta-language cannot implement "Hello World").
Thus coding theory should imply that this should lead to more succinct utte=
rances (in general).
From this point of view, language design is about striking a balance betwee=
n the low input bandwidth of neurotypical human brains (thus compression is=
 needed, i.e. the language encourages succinct programs) and the limited pr=
ocessing power of neurotypical human brains (thus decompression speed is ne=
eded, i.e. it should be obvious what something expands to).


Regards,
ZmnSCPxj