1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
|
Return-Path: <ZmnSCPxj@protonmail.com>
Received: from smtp1.osuosl.org (smtp1.osuosl.org [IPv6:2605:bc80:3010::138])
by lists.linuxfoundation.org (Postfix) with ESMTP id 22FDFC000A
for <bitcoin-dev@lists.linuxfoundation.org>;
Fri, 16 Apr 2021 14:35:44 +0000 (UTC)
Received: from localhost (localhost [127.0.0.1])
by smtp1.osuosl.org (Postfix) with ESMTP id 048F783BAC
for <bitcoin-dev@lists.linuxfoundation.org>;
Fri, 16 Apr 2021 14:35:44 +0000 (UTC)
X-Virus-Scanned: amavisd-new at osuosl.org
X-Spam-Flag: NO
X-Spam-Score: 0.401
X-Spam-Level:
X-Spam-Status: No, score=0.401 tagged_above=-999 required=5
tests=[BAYES_50=0.8, DKIM_SIGNED=0.1, DKIM_VALID=-0.1,
DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, FREEMAIL_FROM=0.001,
FROM_LOCAL_NOVOWEL=0.5, RCVD_IN_DNSWL_LOW=-0.7,
RCVD_IN_MSPIKE_H4=0.001, RCVD_IN_MSPIKE_WL=0.001,
SPF_HELO_PASS=-0.001, SPF_PASS=-0.001]
autolearn=ham autolearn_force=no
Authentication-Results: smtp1.osuosl.org (amavisd-new);
dkim=pass (1024-bit key) header.d=protonmail.com
Received: from smtp1.osuosl.org ([127.0.0.1])
by localhost (smtp1.osuosl.org [127.0.0.1]) (amavisd-new, port 10024)
with ESMTP id 8pCK_DLMnIZe
for <bitcoin-dev@lists.linuxfoundation.org>;
Fri, 16 Apr 2021 14:35:39 +0000 (UTC)
X-Greylist: domain auto-whitelisted by SQLgrey-1.8.0
Received: from mail-40130.protonmail.ch (mail-40130.protonmail.ch
[185.70.40.130])
by smtp1.osuosl.org (Postfix) with ESMTPS id 6759E80FF9
for <bitcoin-dev@lists.linuxfoundation.org>;
Fri, 16 Apr 2021 14:35:39 +0000 (UTC)
Date: Fri, 16 Apr 2021 14:35:31 +0000
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=protonmail.com;
s=protonmail; t=1618583735;
bh=aPF3ss4TCAUlYN3IT8OLO7V63y3zaJRvHTHv10+wZ2U=;
h=Date:To:From:Reply-To:Subject:In-Reply-To:References:From;
b=v9//JLzkgLHWnj7ChBHJBAM3FIv1qKG+uVnzqpApb1ihJXLGAwfhDjn5QputTNT8h
jlvN/nPRBAyw8j1wlJ7TPNxU2iY/6qEvz4+BsAHp+NYaDsdMYKhSZxvIpTqHnEiv99
SKjP8zO4wvxVj3kjatztnv6axaYccjujEKCUUytE=
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)
X-BeenThere: bitcoin-dev@lists.linuxfoundation.org
X-Mailman-Version: 2.1.15
Precedence: list
List-Id: Bitcoin Protocol Discussion <bitcoin-dev.lists.linuxfoundation.org>
List-Unsubscribe: <https://lists.linuxfoundation.org/mailman/options/bitcoin-dev>,
<mailto:bitcoin-dev-request@lists.linuxfoundation.org?subject=unsubscribe>
List-Archive: <http://lists.linuxfoundation.org/pipermail/bitcoin-dev/>
List-Post: <mailto:bitcoin-dev@lists.linuxfoundation.org>
List-Help: <mailto:bitcoin-dev-request@lists.linuxfoundation.org?subject=help>
List-Subscribe: <https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev>,
<mailto:bitcoin-dev-request@lists.linuxfoundation.org?subject=subscribe>
X-List-Received-Date: Fri, 16 Apr 2021 14:35:44 -0000
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
|
