diff options
| author | ZmnSCPxj <ZmnSCPxj@protonmail.com> | 2021-04-16 14:35:31 +0000 |
|---|---|---|
| committer | bitcoindev <bitcoindev@gnusha.org> | 2021-04-16 14:35:44 +0000 |
| commit | 7f89af60fe33fc6d69ef058cfd01e95900a28116 (patch) | |
| tree | 193ba6cf75eea1ca2d6473d14b5b2d28fb48ba65 | |
| parent | c30f71d923f40c1b24688d861f14b78f609ae4b9 (diff) | |
| download | pi-bitcoindev-7f89af60fe33fc6d69ef058cfd01e95900a28116.tar.gz pi-bitcoindev-7f89af60fe33fc6d69ef058cfd01e95900a28116.zip | |
Re: [bitcoin-dev] Designing Bitcoin Smart Contracts with Sapio (available on Mainnet today)
| -rw-r--r-- | 82/498e036eb52b79c9111e013797e2830cf06ecd | 174 |
1 files changed, 174 insertions, 0 deletions
diff --git a/82/498e036eb52b79c9111e013797e2830cf06ecd b/82/498e036eb52b79c9111e013797e2830cf06ecd new file mode 100644 index 000000000..617be645f --- /dev/null +++ b/82/498e036eb52b79c9111e013797e2830cf06ecd @@ -0,0 +1,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 + |