From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from smtp1.osuosl.org (smtp1.osuosl.org [IPv6:2605:bc80:3010::138]) by lists.linuxfoundation.org (Postfix) with ESMTP id 22FDFC000A for ; 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 ; 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 ; 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 ; 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 , Bitcoin Protocol Discussion From: ZmnSCPxj Reply-To: ZmnSCPxj Message-ID: <9jIB9EQTV4UY5OieVmn5P791NA3Oq3WJ2EXaG0fqscLxQx913zD6ds46YHXAie9JvKuZ0CpiRUUiXjHuosfyuzFdlQhgOUeiolZaca8_zQA=@protonmail.com> In-Reply-To: References: 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 List-Unsubscribe: , List-Archive: List-Post: List-Help: List-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