# Bitcoin scripting language extensions, collaboration requested

## Mark Friedenbach — 2014-01-28 23:34:05

    -----BEGIN PGP SIGNED MESSAGE-----

    Hash: SHA1

    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

    -----BEGIN PGP SIGNATURE-----

    Version: GnuPG v1.4.14 (GNU/Linux)

    Comment: GPGTools - http://gpgtools.org

    Comment: Using GnuPG with Thunderbird - http://www.enigmail.net/

    iQIcBAEBAgAGBQJS6D5pAAoJEAdzVfsmodw4OD4QAK3PrzboP91SfIsvUbPfTHaS

    r14eNHNlAQjS0Hdc7vwDEsMsZVB2G4+O+7dpxY1T/YTCM236wPD9q4c85WL35QFJ

    CGXdhNeUUYwfPsS9NUC8wyFgm0fC/y6I8dhmZ2OzfUR4SDJF785UZE7FAlFg6zYK

    lNKX4jN4Q6XKte/hmvCruDhZ8h3DkwUBkVrc2YqEYtaRRm6VUEXA/tA0tiIXNqfC

    FznADvGMxwgH4QamGErfA1cslqbRUtbjneXTpnC9tNmDLZSpQ2HfuYqyGVNupfLU

    4dXPNXY/T63HVABhTy+ERSPy19gh6O9WS0XlwwPPoYUuAFN/H285LeOTJC0AgmaL

    0VKP0iKkBmyMw+AysVZxS6hHK/yl14+Rmq6SZb322qv/hf3paPEgUZGKufcH1IvF

    0LFIZHK+cWaJIigUzuco8jHao0CPaCiV0rDJkK8ZFFY4Ox5Q+PbiQ0tiDFWzMIiL

    Rni34wzQKpp7kowcTTbrPNrKeIyxkKG2krQufh4qtRmOOxjOHgdHWsEuThmrAfGc

    hZWwd3SLCV0Abu2WOKoZpikYTgQOgOHEDiRYTRHPz/RH9rql15EFRdSFf1zFIiN4

    btFKKQQjzgP9KHgMzRl6tJ76PR2HE1xq0BVZdxnQDlWgZnlnvsHMDG5Z2X4v4ZUB

    vGJV4ww+Rz9SVQszIHpr

    =5kz9

    -----END PGP SIGNATURE-----

## Matt Hellige — 2014-01-29 04:05:47

    On Tue, Jan 28, 2014 at 5:34 PM, Mark Friedenbach <mark@...> wrote:

     >

    > 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.

    >

     Hi Mark...

    This is an interesting project, although I doubt I could contribute

    much. I know a little bit, but not a lot, about Bitcoin. I know that

    the protocol incorporates some scripting capabilities, but don't know

    too much about them. Your requirements are sensible, although I feel

    like your goals for the type system may pose very significant

    challenges. I do wonder why you restrict yourself to

    concatenative/stack-based designs. It seems like you may also want to

    consider a more traditional (i.e., applicative) total functional

    programming language design, since there is significantly more work in

    type systems there that might be more directly applicable.

    Anyway, I'd be interested to follow discussion of this project, if

    possible. Is there a mailing list or similar where people are (or will

    be) talking about this?

    Best of luck...

    Matt

## Jon Purdy — 2014-01-29 05:50:44

    On Tue, Jan 28, 2014 at 8:05 PM, Matt Hellige <matt@...> wrote:

          On Tue, Jan 28, 2014 at 5:34 PM, Mark Friedenbach <mark@...> wrote:

    >

    > 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.

    >

    Hi Mark...

    This is an interesting project, although I doubt I could contribute

    much. I know a little bit, but not a lot, about Bitcoin. I know that

    the protocol incorporates some scripting capabilities, but don't know

    too much about them. Your requirements are sensible, although I feel

    like your goals for the type system may pose very significant

    challenges. I do wonder why you restrict yourself to

    concatenative/stack-based designs. It seems like you may also want to

    consider a more traditional (i.e., applicative) total functional

    programming language design, since there is significantly more work in

    type systems there that might be more directly applicable.
    Concatenative languages have a simpler execution model, for one thing, and are easy to make predictable about resource usage.

    Anyway, I'd be interested to follow discussion of this project, if

    possible. Is there a mailing list or similar where people are (or will

    be) talking about this?

    This would be the one, I reckon. I have emailed back and forth with Mark a bit and am quite interested in the project, seeing as how I’ve been working on type systems and concatenative languages in my spare time for a couple years now.

    Of course, I also don’t know much about Bitcoin (nor cryptography, nor finance), but am perfectly willing to learn.

## Robbert van Dalen — 2014-01-29 08:12:02

    Hi,
    I’ve developed (but stopped maintaining) the Enchilada programming 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 semantics2) 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 <mark@...> wrote:

    -----BEGIN PGP SIGNED MESSAGE-----
    Hash: SHA1

    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
    -----BEGIN PGP SIGNATURE-----
    Version: GnuPG v1.4.14 (GNU/Linux)
    Comment: GPGTools - http://gpgtools.org
    Comment: Using GnuPG with Thunderbird - http://www.enigmail.net/

    iQIcBAEBAgAGBQJS6D5pAAoJEAdzVfsmodw4OD4QAK3PrzboP91SfIsvUbPfTHaS
    r14eNHNlAQjS0Hdc7vwDEsMsZVB2G4+O+7dpxY1T/YTCM236wPD9q4c85WL35QFJ
    CGXdhNeUUYwfPsS9NUC8wyFgm0fC/y6I8dhmZ2OzfUR4SDJF785UZE7FAlFg6zYK
    lNKX4jN4Q6XKte/hmvCruDhZ8h3DkwUBkVrc2YqEYtaRRm6VUEXA/tA0tiIXNqfC
    FznADvGMxwgH4QamGErfA1cslqbRUtbjneXTpnC9tNmDLZSpQ2HfuYqyGVNupfLU
    4dXPNXY/T63HVABhTy+ERSPy19gh6O9WS0XlwwPPoYUuAFN/H285LeOTJC0AgmaL
    0VKP0iKkBmyMw+AysVZxS6hHK/yl14+Rmq6SZb322qv/hf3paPEgUZGKufcH1IvF
    0LFIZHK+cWaJIigUzuco8jHao0CPaCiV0rDJkK8ZFFY4Ox5Q+PbiQ0tiDFWzMIiL
    Rni34wzQKpp7kowcTTbrPNrKeIyxkKG2krQufh4qtRmOOxjOHgdHWsEuThmrAfGc
    hZWwd3SLCV0Abu2WOKoZpikYTgQOgOHEDiRYTRHPz/RH9rql15EFRdSFf1zFIiN4
    btFKKQQjzgP9KHgMzRl6tJ76PR2HE1xq0BVZdxnQDlWgZnlnvsHMDG5Z2X4v4ZUB
    vGJV4ww+Rz9SVQszIHpr
    =5kz9
    -----END PGP SIGNATURE-----

## Mark Friedenbach — 2014-01-31 19:42:02

    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 <mark@...

    > <mailto:mark@...>> 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

    >>

    >>

    >

    >

## William Tanksley, Jr — 2014-02-01 17:53:24

    Robbert, your SPREAD language is also interesting (assuming I remember

    the name right), especially since it has a large non-Turing-complete

    subset, which helps in analysis.

## — 2014-02-02 11:56:17

    I emailed you directly, but in case it went astray I thought I should reply with the substance of that here, too.

    First off, I'll draw your attention to my own work on Furphy at http://users.beagle.com.au/peterl/furphy.html, currently on hiatus because of my other priorities, so you can see where there's any overlap between that and your needs (it won't be 100%, maybe not even 50%, but looking will help firm up our insights). I should mention, the code quotation system in Furphy is just a syntactic sugar layer and is not part of the underlying machinery; that reduces run time issues and some implementation issues.

    Next, I'll ask about your strong typing requirement. The thing is, if the typing has to be deeply integrated into the virtual machine, it can be done, but that in turn makes it complex (working against your RISC simplicity philosophy). On the other hand, if it can be part of a layer on top of a simple virtual machine, everything will be much simpler and better separated (read: modularised the right way), but that may present problems if it opens up a gap hackers might be able pry into, depending on just what else your eventual design ends up committing to. [Addendum: the easiest way to provide typing in the source is to provide it in an underlying layer, then have the compiler recognise what would be much like stack effect comments in Forth and use those both as run time assertions (which could be disabled) and as compile time things to confirm and to drive the types to use.]

    On what I've seen so far, I'd suggest you implement a prototype scripting language to hold up against your thinking and firm it up. For that, I'd suggest something Forth-ish (maybe even Furphy!), implemented along the lines of Eforth or Hforth for convenience rather than optimised for speed in the prototype. It should also be implemented on top of the Oberon virtual machine or similar (google Wirth and Oberon for details). That's both because that lets it snarf all sorts of useful things like its strong, extensible typing system and its garbage collection, and because the Oberon virtual machine is already accessible, portable(ish) and reasonably proven and robust - all things that would save reinventing the wheel for a mere prototype scripting language.

    As you see, this is just focussing on your topics (a) and (b) at this stage, as you suggested. Your feedback would be welcome.

## Mark Friedenbach — 2014-02-04 01:44:36

    -----BEGIN PGP SIGNED MESSAGE-----

    Hash: SHA1

    Thank you, I will add Furby to the growing list of languages to steal

    ideas from :)

    A strongly enforced decidable type system actually makes the execution

    model simpler - there are all sorts of exceptional circumstances which

    simply cannot happen because the type system prevents such scripts

    from even being executed. “Implementation defined” is a phrase that

    does not exist in global consensus systems like bitcoin, so avoiding

    edge cases entirely (“what happens when you divide by a string?”)

    greatly simplifies the situation. Additionally, being able to generate

    succinct proofs about a script is advantageous to this particular

    application as these proofs may be necessary for coins with attached

    conditions to be accepted by a wallet application. Again, a strong,

    decidable type system is what provides this capability.

    The plan right now is to implement the script interpreter using a

    relatively safe subset of C++, and try to keep the entire

    implementation (including type inference & checking) at under 500

    lines of code. Keeping the interpreter simple enough to be so succinct

    in a compiled, imperative language will help minimize potential

    consensus-affecting implementation errors. Even Oberon would be an

    unsatisfactorily large external dependency (as all implementations

    would have to be bug-for-bug compatible with the specific version of

    the VM we choose).

    Does that make sense?

    Kind regards,

    Mark Friedenbach

     On 02/02/2014 03:56 AM, pml540114@... wrote:

    >

    >

    > I emailed you directly, but in case it went astray I thought I

    > should reply with the substance of that here, too.

    >

    > First off, I'll draw your attention to my own work on Furphy at

    > http://users.beagle.com.au/peterl/furphy.html, currently on hiatus

    > because of my other priorities, so you can see where there's any

    > overlap between that and your needs (it won't be 100%, maybe not

    > even 50%, but looking will help firm up our insights). I should

    > mention, the code quotation system in Furphy is just a syntactic

    > sugar layer and is not part of the underlying machinery; that

    > reduces run time issues and some implementation issues.

    >

    > Next, I'll ask about your strong typing requirement. The thing is,

    > if the typing has to be deeply integrated into the virtual machine,

    > it can be done, but that in turn makes it complex (working against

    > your RISC simplicity philosophy). On the other hand, if it can be

    > part of a layer on top of a simple virtual machine, everything will

    > be much simpler and better separated (read: modularised the right

    > way), but that may present problems if it opens up a gap hackers

    > might be able pry into, depending on just what else your eventual

    > design ends up committing to. [Addendum: the easiest way to provide

    > typing in the source is to provide it in an underlying layer, then

    > have the compiler recognise what would be much like stack effect

    > comments in Forth and use those both as run time assertions (which

    > could be disabled) and as compile time things to confirm and to

    > drive the types to use.]

    >

    > On what I've seen so far, I'd suggest you implement a prototype

    > scripting language to hold up against your thinking and firm it up.

    > For that, I'd suggest something Forth-ish (maybe even Furphy!),

    > implemented along the lines of Eforth or Hforth for convenience

    > rather than optimised for speed in the prototype. It should also be

    > implemented on top of the Oberon virtual machine or similar (google

    > Wirth and Oberon for details). That's both because that lets it

    > snarf all sorts of useful things like its strong, extensible typing

    > system and its garbage collection, and because the Oberon virtual

    > machine is already accessible, portable(ish) and reasonably proven

    > and robust - all things that would save reinventing the wheel for a

    > mere prototype scripting language.

    >

    > As you see, this is just focussing on your topics (a) and (b) at

    > this stage, as you suggested. Your feedback would be welcome.

    >

    >

    -----BEGIN PGP SIGNATURE-----

    Version: GnuPG v1.4.14 (GNU/Linux)

    Comment: GPGTools - http://gpgtools.org

    Comment: Using GnuPG with Thunderbird - http://www.enigmail.net/

    iQIcBAEBAgAGBQJS8EYBAAoJEAdzVfsmodw4O5cP/A+gDtAC6Rp3/i/5aAYUyC/i

    Gxcj4dpnuYfemPY81xtOHDx4nYL6VS7ElvF8+tZoEZW+zJ9EMX45WiMHUIurTFo5

    SkTZiexNLBu2BhXA3HfsvIL3kuwWkwu36DgIBue0STCDr7AEkjXbPvE6VttSCVsF

    kAjjSdDnA8X6DqvVXN07fm826b+dq2L9Eht1ATwAKwvoZpfwxl/5KkJ7RHp5b3u6

    3DoMrXF3ayY77h7/qOgxMdLTNbcVaaO76qCv8p/pJCdElAGTS4m0VrH0HZraf586

    o08FG+ab/cZaJO50OAK9Pc3BnaFHkfcVVqk9lrH+osDdaHcQT6EdiRtzTpYcHEJr

    K50Zm6lGJb5zwgfwyKt3Yq0qBo6AYe/HRjMIDD6qmxnq4YWY7crY1GMNuD8nrEGR

    iAyLgwhpe3oRYCNbJsauUbs5aC5XoieUkEc7Se7ww53oGdX7s/cwyeMBc488deM+

    QvUt1tXcehaPGWM72kxK0I6UCAsN6lH3+dQOkmorVtFd05cP3Y8H0TVHTsZqE59V

    ICuuO1L0sfy56OMRBQrep8jqiFQKW3TY6RBJvDO9ptt6NpDtTsJnshySy2bL3GLP

    cdXCYBvL6XW2zHyk2u4JB7Kmtpzlf9gdIo4xWWWnHLAqSDxK5bzf8AZv8iVugcGy

    hN7JecfAVTc6kZcWoBoq

    =sAX5

    -----END PGP SIGNATURE-----

## Mark Friedenbach — 2014-02-04 02:06:54

    -----BEGIN PGP SIGNED MESSAGE-----

    Hash: SHA1

    SPREAD is very interesting indeed. I'm not sure yet how it applies to

    this bitcoin extension, but I am thinking of future project I have in

    mind of a probabilistic programming language. In such a language

    storing how values were derived becomes vitally important - as you

    perform updates of the knowledge base, you need to update also any

    facts derived from those being updated.

    Do you know if there is more info on the web about SPREAD? My

    Google-fu is having a little trouble finding anything more than the

    announcement post.

    Mark

     On 02/01/2014 09:53 AM, William Tanksley, Jr wrote:

    >

    >

    > Robbert, your SPREAD language is also interesting (assuming I

    > remember the name right), especially since it has a large

    > non-Turing-complete subset, which helps in analysis.

    >

    >

    -----BEGIN PGP SIGNATURE-----

    Version: GnuPG v1.4.14 (GNU/Linux)

    Comment: GPGTools - http://gpgtools.org

    Comment: Using GnuPG with Thunderbird - http://www.enigmail.net/

    iQIcBAEBAgAGBQJS8Es+AAoJEAdzVfsmodw4OrEP/3vFORbYTxu05CGa/2iTnWWS

    ZYvKTIs1cwZ33i/fk+o8OBzJjAl1otIVImAuQSQXmDQgDa9JxsttdgyvZIzTAyoq

    AHg963iKpsq2NlMyuBV0XZnd6JjxQD+9l5DrqRM02G0c/8+usB2c1eQYUAuWfloB

    4UBsMms13ghxROIkfgYN5sCz3KCndG4VZTh4OWdrXa6CeP17DqRRWYdKOoen9xDa

    Fu6yAPK4gNfpjGzMlTbfwkoYon5DZw8k+YV1xi7Vcw7GWNOmdMU6Zr/vBoV0YiHe

    2Ov8w4pUT6tuzkD2bfsxs6Mho5f6qt9dvEO9Kijq5cKulrwQWQvabfXWedJhKqyc

    JmBu4T3S590aBpsWN3O7rYqMVzkjkqglxmVa6NMHcebKu3kanV4yes3M9pYUsnxO

    Xtgpa6DWPvkaY83AaP2EE1osWo6yJB55tni/p+HD/kGK6KhW8/vF+pK+7UERBhVz

    /7DLVTBGSymjYSR+/6fosJ3GRkXM5NjSaUkCgqt6XFlmxsBjjCKON58CWZs2xG/q

    Dpe6NVPGS61Q6AKV+DyBSBdOZb94wA34bPKCkg8DAxKzpmHy/UAKg1p5laNZN9FZ

    j1VnteG1YpFV3wQ/TIgdvL8El+Tba9/Xq4fru25EysNVGZQs8I3QD6E1P3FJwzrH

    vwROFxE/CuMwg0GE0Jur

    =7tIw

    -----END PGP SIGNATURE-----

## William Tanksley, Jr — 2014-02-04 06:40:02

    http://oercode.blogspot.nl/ has some info.
    -Wm
     On Feb 3, 2014 6:06 PM, "Mark Friedenbach" <mark@...> wrote:

    -----BEGIN PGP SIGNED MESSAGE-----

    Hash: SHA1

    SPREAD is very interesting indeed. I'm not sure yet how it applies to

    this bitcoin extension, but I am thinking of future project I have in

    mind of a probabilistic programming language. In such a language

    storing how values were derived becomes vitally important - as you

    perform updates of the knowledge base, you need to update also any

    facts derived from those being updated.

    Do you know if there is more info on the web about SPREAD? My

    Google-fu is having a little trouble finding anything more than the

    announcement post.

    Mark

    On 02/01/2014 09:53 AM, William Tanksley, Jr wrote:

    >

    >

    > Robbert, your SPREAD language is also interesting (assuming I

    > remember the name right), especially since it has a large

    > non-Turing-complete subset, which helps in analysis.

    >

    >

    -----BEGIN PGP SIGNATURE-----

    Version: GnuPG v1.4.14 (GNU/Linux)

    Comment: GPGTools - http://gpgtools.org

    Comment: Using GnuPG with Thunderbird - http://www.enigmail.net/

    iQIcBAEBAgAGBQJS8Es+AAoJEAdzVfsmodw4OrEP/3vFORbYTxu05CGa/2iTnWWS

    ZYvKTIs1cwZ33i/fk+o8OBzJjAl1otIVImAuQSQXmDQgDa9JxsttdgyvZIzTAyoq

    AHg963iKpsq2NlMyuBV0XZnd6JjxQD+9l5DrqRM02G0c/8+usB2c1eQYUAuWfloB

    4UBsMms13ghxROIkfgYN5sCz3KCndG4VZTh4OWdrXa6CeP17DqRRWYdKOoen9xDa

    Fu6yAPK4gNfpjGzMlTbfwkoYon5DZw8k+YV1xi7Vcw7GWNOmdMU6Zr/vBoV0YiHe

    2Ov8w4pUT6tuzkD2bfsxs6Mho5f6qt9dvEO9Kijq5cKulrwQWQvabfXWedJhKqyc

    JmBu4T3S590aBpsWN3O7rYqMVzkjkqglxmVa6NMHcebKu3kanV4yes3M9pYUsnxO

    Xtgpa6DWPvkaY83AaP2EE1osWo6yJB55tni/p+HD/kGK6KhW8/vF+pK+7UERBhVz

    /7DLVTBGSymjYSR+/6fosJ3GRkXM5NjSaUkCgqt6XFlmxsBjjCKON58CWZs2xG/q

    Dpe6NVPGS61Q6AKV+DyBSBdOZb94wA34bPKCkg8DAxKzpmHy/UAKg1p5laNZN9FZ

    j1VnteG1YpFV3wQ/TIgdvL8El+Tba9/Xq4fru25EysNVGZQs8I3QD6E1P3FJwzrH

    vwROFxE/CuMwg0GE0Jur

    =7tIw

    -----END PGP SIGNATURE-----

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

    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:

        concatenative-digest@yahoogroups.com

        concatenative-fullfeatured@yahoogroups.com

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

        concatenative-unsubscribe@yahoogroups.com

    <*> Your use of Yahoo Groups is subject to:

        http://info.yahoo.com/legal/us/yahoo/utos/terms/

## — 2014-02-05 00:37:18

    Furphy, not Furby.

    I wasn't trying to say that your product should be written in the Oberon language, or that the prototype I suggested should be written in the Oberon language. What I had in mind was that you should mock up a prototype to see what it looked like and how it worked, only not as a low level thing in assembler or some systems language like the C++ you have in mind, all on a low base, but as a low level thing on top of the virtual machine that the Oberon system provides, that the Oberon language compiles for - but not using that language at all, just using its support platform, the virtual machine. That way, you would be able to fine tune what you implemented and be able to see what is involved with that, but the virtual machine would save you implementing various things as it already gives them to the Oberon language. Those things include snarfing the garbage collection and snarfing implementing a powerful type system. Your concerns about getting Oberon everywhere won't come up, because I wasn't suggesting at all that you implement the main thing that way, just that you set up a prototype that way in just one place under your control, and only to see how it all - your own ideas and other people's suggestions, not just mine - comes together. Once your ideas are firmed up, you should throw Oberon away completely and do something fully under your control, just the way you outlined - but that comes later. PML.

## John Nowak — 2014-02-05 20:22:23

    On 01/29/2014 12:50 AM, Jon Purdy wrote:

     > Concatenative languages have a simpler execution model, for one thing,

    > and are easy to make predictable about resource usage.

     First-order applicative languages are easy to give exact resource bounds

    for if you disallow recursion and dynamic allocation. This has been done

    quite successfully already (e.g. SPARK Ada).

    In contrast, a language like Joy or Enchilada is almost certainly not a

    good fit as you'll be stuck with dynamic allocation and (presumably)

    garbage collection. Enchilada in particular is also lazy which turns

    space usage into a non-local property.

    While it is certainly possible to design a stack-based language with

    total functions and bounded resource utilization, I don't think it would

    offer any benefit over an applicative language for the purpose Mark

    describes.

    - jn

## Jon Purdy — 2014-02-05 21:43:25

    First-order applicative languages are easy to give exact resource bounds

    for if you disallow recursion and dynamic allocation. This has been done

    quite successfully already (e.g. SPARK Ada).
    In a total higher-order language, you sacrifice less but can still get a tight upper bound.
    Disallowing general recursion by default is a good idea. We could allow the usual “map”, “fold”, and “filter” combinators, but place an execution limit on scripts that would use “fix”.

    In contrast, a language like Joy or Enchilada is almost certainly not a

    good fit as you'll be stuck with dynamic allocation and (presumably)

    garbage collection. Enchilada in particular is also lazy which turns

    space usage into a non-local property.

    Right. I think we need eager evaluation and heavy restrictions on dynamic allocation.
    Mark’s mention of “funding” more resource-intensive scripts with more Bitcoin seems the key notion here. If you want a bigger bigint, you need deeper pockets.

    While it is certainly possible to design a stack-based language with

    total functions and bounded resource utilization, I don't think it would

    offer any benefit over an applicative language for the purpose Mark

    describes.

    A stack model is largely a convenience. Keep in mind that this is a bytecode, not a surface language.

## William Tanksley, Jr — 2014-02-05 21:45:08

    John Nowak <john@...> wrote:

     > Jon Purdy wrote:

    >> Concatenative languages have a simpler execution model, for one thing,

    >> and are easy to make predictable about resource usage.

    > First-order applicative languages are easy to give exact resource bounds

    > for if you disallow recursion and dynamic allocation. This has been done

    > quite successfully already (e.g. SPARK Ada).

     SPARK Ada should be mentioned, and I hope the Bitcoin people have

    looked at it (Mark?). However, it gains its abilities not by being

    first-order applicative, but rather by having a strong proof language

    tied to a decent and well-known programming language with a

    non-ambiguous subset specification.

     > In contrast, a language like Joy or Enchilada is almost certainly not a

    > good fit as you'll be stuck with dynamic allocation and (presumably)

    > garbage collection. Enchilada in particular is also lazy which turns

    > space usage into a non-local property.

     This is true.

     > While it is certainly possible to design a stack-based language with

    > total functions and bounded resource utilization, I don't think it would

    > offer any benefit over an applicative language for the purpose Mark

    > describes.

     I'm not so sure about that.

     > - jn

     -Wm

## John Nowak — 2014-02-05 22:37:47

    On 02/05/2014 04:43 PM, Jon Purdy wrote:

     > First-order applicative languages are easy to give exact resource bounds

    > for if you disallow recursion and dynamic allocation. This has been done

    > quite successfully already (e.g. SPARK Ada).

    >

    > In a total higher-order language, you sacrifice less but can still get a

    > tight upper bound.

     First-order languages without recursion are trivial in this regard

    because you just go through the call tree and total up the amount of

    memory required for the stack at its highest point. You cannot get the

    same thing so easily with a higher-order language, and I'm not aware of

    any existing or proposed higher-order language that offers it. If you

    know of one, please share.

     > A stack model is largely a convenience. Keep in mind that this is a

    > bytecode, not a surface language.

     If it is, I think I missed something: I thought this was for a contract

    scripting language as per the title. My impression was that people would

    be writing these contracts by hand -- or, if they're generated with some

    tool, reading them at the very least -- hence my tentative preference

    for a simple and readable applicative language.

    - jn

## John Nowak — 2014-02-05 22:42:53

    On 02/05/2014 04:45 PM, William Tanksley, Jr wrote:

     >> First-order applicative languages are easy to give exact resource bounds

    >> for if you disallow recursion and dynamic allocation. This has been done

    >> quite successfully already (e.g. SPARK Ada).

    >

    > SPARK Ada should be mentioned, and I hope the Bitcoin people have

    > looked at it (Mark?). However, it gains its abilities not by being

    > first-order applicative, but rather by having a strong proof language

    > tied to a decent and well-known programming language with a

    > non-ambiguous subset specification.

     The ability to easily calculate resource bounds is precisely due to the

    restriction to first-order, recursion-free, allocation-free code: You

    can just go through the call tree statically and calculate the maximum

    height of the stack. The same thing would be possible even if it offered

    no support for proof.

    Some of its other abilities I did not mention however, e.g. static array

    bounds checking, certainly do require user-provided proofs in some cases.

    - jn

## John Cowan — 2014-02-05 23:11:02

    John Nowak scripsit:

     > The ability to easily calculate resource bounds is precisely due to the

    > restriction to first-order, recursion-free, allocation-free code: You

    > can just go through the call tree statically and calculate the maximum

    > height of the stack.

     Indeed, it hardly even makes sense to speak of the stack; you just allocate

    static locations for all the arguments of all the procedures, the traditional

    implementation strategy for Fortran 66 and down.  If memory is very tight,

    you might do better with a little analysis showing that some procedures

    cannot call one another and therefore can share storage, though traditional

    Fortran left that up to the programmer with the infamous EQUIVALENCE

    declaration.

    --

    John Cowan <cowan@...>             http://www.ccil.org/~cowan

    Sir, I quite agree with you, but what are we two against so many?

        --George Bernard Shaw,

             to a man booing at the opening of _Arms and the Man_

## chris glur — 2014-02-03 01:32:49

    > Next, I'll ask about your strong typing requirement. The thing is, if

    > the typing has to be deeply integrated into the virtual machine, it can

    > be done, but that in turn makes it complex (working against your RISC

    > simplicity philosophy).

     I'd like to see the hidden assumptions, of the value of strong typing,

    spelled-out:

    * to specify, exactly, the byte-format of the data-structures, so as to

     keep control of the project, and avoid the system <taking over> and

     causing unexpected results ?

    --

     > It should also be implemented on top of the Oberon virtual machine or

    > similar (google Wirth and Oberon for details). That's both because that

    > lets it snarf all sorts of useful things like its strong, extensible typing

    > system and its garbage collection, and because the Oberon virtual machine

    > is already accessible, portable(ish) and reasonably proven and robust -

    > all things that would save reinventing the wheel for a mere prototype

    > scripting language.

     What am I missing ?!

    Since the 90's when my ISP told that I couldn't use Win3 any longer,

    and would have to buy W95, I said "srew-you" and found linux and

    ETHOberon. Since then I've been using ETHO [linux based mostly recently]

    for 200 days per year. The mail-list doesn't mention "Oberon virtual machine".

    Yes: in the 70s there was the UnivSanDiegoPseudoCode system Pascal

    implementation.

    Using Wirth's simplest recursive descent compiler to generate P-code for a

    VM, which had only a few virtual-instruction was an easy way to port a

    HiLevelLanguage onto new microprocessors, before forth became well known.

    It seems strange that Bitcoin is asking these questions.

    I thought it was established & matured?

    That ETHO's HumanComputeInterface is superb, but apparently unpopular, is

    also strange to me. Since I lost my <basic ISP> who could handle proper

    ETHO-based email, gmail has been a disaster.

    == Chris Glur.

## Jorge Timón — 2014-03-05 19:21:13

    First, I want to thank you all for helping us on this.

     On 2/5/14, John Nowak <john@...> wrote:

    > The ability to easily calculate resource bounds is precisely due to the

    > restriction to first-order, recursion-free, allocation-free code: You

    > can just go through the call tree statically and calculate the maximum

    > height of the stack. The same thing would be possible even if it offered

    > no support for proof.

    This sounds very good.

    I don't think we need dynamic allocation, you should be able to do

    anything just using the stack.

    Recursion seems intuitively dangerous for attacks like loop bombs.

    On the bytecode vs readable language discussion, although there's no

    reason why someone couldn't use a more powerful language that gets

    compiled to the base scripting, probably most contracts will be

    written by hand. So although readability is not the first priority, it

    would certainly be something nice to have.

    One thing I'm not sure it's being considered related to requirement d

    (merkle tree structure) is the ability for a script to select concrete

    parts from another script (we generically call these "extrospection

    operations" which may refer to other scripts and other merkle tree

    structures in the system like the unspent transaction outputs set

    UTXO).

    I'm sorry this probably sounds too abstract, probably we should start

    with some simpler examples first after Mark writes the set of basic

    crypto primitives.

    To get a sense of what's now possible, you can read this:

    https://en.bitcoin.it/wiki/Script

    Well, most operands are actually currently disabled, but still there

    are some simple allowed transactions at the end.

    This is probably interesting to read as well (although some of them

    aren't actually currently allowed either):

    https://en.bitcoin.it/wiki/Contracts