-----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-----
On Tue, Jan 28, 2014 at 5:34 PM, Mark Friedenbach <mark@...> wrote:
>Hi Mark...
> 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.
>
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
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:Hi Mark...
>
> 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.
>
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.
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 functionI’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-----
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
>>
>>
>
>
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.
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 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-----
-----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-----
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/
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.
On 01/29/2014 12:50 AM, Jon Purdy wrote:
> Concatenative languages have a simpler execution model, for one thing,First-order applicative languages are easy to give exact resource bounds
> and are easy to make predictable about resource usage.
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
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.
John Nowak <john@...> wrote:
> Jon Purdy wrote:SPARK Ada should be mentioned, and I hope the Bitcoin people have
>> 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).
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 aThis is true.
> 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 withI'm not so sure about that.
> 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-Wm
On 02/05/2014 04:43 PM, Jon Purdy wrote:
> First-order applicative languages are easy to give exact resource boundsFirst-order languages without recursion are trivial in this regard
> 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.
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 aIf it is, I think I missed something: I thought this was for a contract
> bytecode, not a surface language.
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
On 02/05/2014 04:45 PM, William Tanksley, Jr wrote:
>> First-order applicative languages are easy to give exact resource boundsThe ability to easily calculate resource bounds is precisely due to the
>> 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.
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 Nowak scripsit:
> The ability to easily calculate resource bounds is precisely due to theIndeed, it hardly even makes sense to speak of the stack; you just allocate
> 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.
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_
> Next, I'll ask about your strong typing requirement. The thing is, ifI'd like to see the hidden assumptions, of the value of strong typing,
> 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).
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 orWhat am I missing ?!
> 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.
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.
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