Re: Bitcoin scripting language extensions, collaboration requested

Thanks Robert, I'll take a look at Enchilada!
Mark

On 01/29/2014 12:12 AM, Robbert van Dalen wrote:
>  
> 
> Hi,
> 
> 
> I’ve developed (but stopped maintaining) the Enchilada programming
> <http://www.enchiladacode.nl> language which more or less covers
> requirements b) c) and d).
> Enchilada is (dynamically) mono-typed and homoiconic: evaluations and
> code are also data.
> 
> Proving things in Enchilada should - to some extend - be possible,
> because of:
> 
> 1) pure (rule) rewriting semantics
> 2) every operator is a pure and total function
> 
> I’m not suggesting that Enchilada is a perfect fit, but I do think some
> of Enchilada’s rationale/design decisions may be of interest to you.
> 
> Cheers,
> Robbert.
> 
> On 29 Jan 2014, at 00:34, Mark Friedenbach <[email protected]
> <mailto:[email protected]>> wrote:
> 
> Hi,
> 
> My name is Mark Friedenbach and I am a bitcoin-core developer [1]. You
> probably know Bitcoin as a peer-to-peer protocol for the digital
> money. What you may not know is that Bitcoin uses a simple,
> Forth-derived but crippled concatenative language for encoding smart
> contracts representing the terms and conditions for transferring
> ownership of digital goods.
> 
> I'm part of a small volunteer team that is looking at ways we can
> extend the Bitcoin protocol so as to be able to perform a broader
> range of financial services. For example, a more expressive scripting
> language could enable attaching conditionals / "covenants" to assets
> which stay with them even as they transfer owners, e.g. a restricted
> buy-back option for an IOU certificate, which lets the debtor pay off
> the loan without requiring permission of the owner of the debt or
> impacting his/her rights in any other way. This is not currently
> possible in Bitcoin.
> 
> We would like to prototype a replacement contract scripting language
> for Bitcoin derived from Joy, or any one of the other purely
> functional concatenative languages I see discussed in this list's
> archives. This is a chance to help secure and extend the capabilities
> of a $10 billion economy, and to make an expressive concatenative
> language which will be used by the financial industry for decades to come.
> 
> There are also some interesting requirements that we must place on
> such a language:
> 
> a. The language must be strongly typed with a decidable type system
> capable of constructing proofs of nontrivial properties. Examples
> beyond ordinary type safety verification might include: proving that
> the scripts requirements can be met solely with knowledge of a set of
> signature-generating private keys, or proving the opposite (that a
> script is unspendable); proving that a script has a constraint
> attached (e.g. cannot be spent before block height N, or simple
> restricted buy-back capability) which can then be pattern matched
> against a whitelist of acceptable constraints.
> 
> b. The script must be simple, as thousands of nodes world-wide running
> multiple implementations will need to reach global consensus over not
> just the outcome of a script, but also some aspects of the execution
> (e.g. an instruction counter). Consensus failures whether due to bugs
> or faulty designs can lead to unsecured payment networks and possible
> losses in the millions of dollars or more. Interpreter escape would be
> absolutely catastrophic. So simple, minimal, but expressive
> architectures with simple fail-safe implementations are to be
> preferred over complex but user-friendly (RISC is better than CISC).
> 
> c. The language must support the various cryptographic primitives
> necessary for performing core bitcoin functions. Mostly this just
> means adding a handful of builtin words for performing strong
> cryptographic hashes and elliptic curve signature verification, but
> there are some requirements on the language design as well, chiefly in
> making decisions about how the stack is represented for hash
> operations and in supporting authenticated data structures as
> primitive types for external state.
> 
> d. Merkle structured compiled form [2]. A script containing quoted
> forms may be considered a hierarchical structure, and Merkle
> compression allows us to reduce such a script to a single root hash
> value (to be placed in the output of a bitcoin transaction) or to
> "prune" execution pathways which are not taken when the script is
> instantiated at spend time, either to compress a large script or to
> provide privacy over the data in branches not taken.
> 
> The requirements (a) and (b) are probably the most interesting for
> this list. I must admit that type theory is outside of my area of
> expertise. I know only enough to know that we need it, but not enough
> to design such a system myself. I imagine that it must also be an
> interesting challenge to design a minimalistic language that is
> trivial to implement, but still capable of generating expressive,
> compact, readable programs.
> 
> If anyone here is interested in collaborating with us, or even just
> sharing their experience in comments, we'd appreciate it very much!
> 
> Happy hacking,
> Mark Friedenbach
> 
> [1]: Bitcoin is a peer-to-peer currency and payment protocol:
> http://bitcoin.org/
> 
> [2]: By analogy to the Merkle hash-tree:
> http://en.wikipedia.org/wiki/Merkle_tree
>>
>>
> 
> 


------------------------------------

Yahoo Groups Links

<*> To visit your group on the web, go to:
    http://groups.yahoo.com/group/concatenative/

<*> Your email settings:
    Individual Email | Traditional

<*> To change settings online go to:
    http://groups.yahoo.com/group/concatenative/join
    (Yahoo! ID required)

<*> To change settings via email:
    [email protected] 
    [email protected]

<*> To unsubscribe from this group, send an email to:
    [email protected]

<*> Your use of Yahoo Groups is subject to:
    http://info.yahoo.com/legal/us/yahoo/utos/terms/