Mark Friedenbach
2014-01-28 23:34:05 UTC
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
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