Does the benefit of it being embeddable on a QR code outweigh the lack of quality of life features like subtraction? Nevertheless, truly an impressive feat that shows how simple computers can be without all these modern API layers.
For one specific purpose, the benefit could be worth it: bootstrapping.
Guix bootstraps from a tiny audited binary, and milliForth could be used for the same purpose.
Imagine bootstrapping a full Linux distro from a milliForth binary and source code for everything. Everything would be fully auditable, no Trusting Trust problem, and a full Software Bill of Materials.
I always thought of FORTH as the #1 hardest to think of uses for, out of all the non-esoteric and non-obsolete languages. That's a really neat application!
Booting from a firmware Forth loader was how the early Sun SunOS (BSD) workstations did their thing - you could hotkey to stop the default OS load and boot from an image on an alternative drive, across a network, or modify the Forth loader to <imagination>
That forth system is also where Device Trees originated. Parts of the Linux kernel driver interface show that heritage in the naming conventions, OF_* == OpenFirmware.
I believe Forth is used quite a bit in the embedded world - or used to be. I read, long ago from the Usenet days, you use it when you don't want to write assembly but C is too "heavy" for your hardware.
Bitcoin's smart contracting language is a Forth variant, and arguably this was a very astute and smart choice by Satoshi.
When designing a multi-party contract, the essential problem is that two people specify the terms they each want to apply to any case in which the funds must be spent, then these two sets of requirements must be merged into a single program. This is, in general, difficult to do securely. We can establish conventions that are relatively easy to follow, but it would be a lot nicer and more powerful if we could syntactically enforce that both sets of requirements are enforced in the combined program.
Concatenative languages like Forth meet this requirement nicely. If you represent the spend requirements as a program, then combining the two programs together in such a way that they both are equally enforce is as simple as literally concatenating the two programs together.
For example, suppose Alice's requirement is that Alice signs the transaction with her key, and Bob's requirement is that Bob signs with his key, and the spending transaction is after some specified time T. Expressed in bitcoin script:
Alice: <AlicePubkey> CHECKSIGVERIFY
Bob: <T> CHECKLOCKTIMEVERIFY DROP <BobPubkey> CHECKSIGVERIFY
The combined script that meets both these sets of requirements is as simple as putting Alice's script, then Bob's, unaltered:
Alice&Bob: <AlicePubkey> CHECKSIGVERIFY <T> CHECKLOCKTIMEVERIFY DROP <BobPubkey> CHECKSIGVERIFY 1
(The `1` at the end is a quirk of bitcoin that it has to finish with a non-zero value on the stack. This combined script could also be simplified in a couple of ways. Also there's a couple of ways in which this can fail in practice. Alice's script could contain OP_RETURN, for example, which causes the entire script to become unspendable. Or a mismatched IF/ELSE. A better designed and strongly typed Forth dialect would fix these issues.)
Bitcoin's Forth is not type checked, but suppose that it were. And furthermore, suppose that it had a powerful dependently typed system that captured various key signing and stack requirements at the type level. It could be used to track not just what a program does, but also the properties of a program. Alice could put a constraint in her program that says "lock time can be no later than April 2024," and this becomes part of both the input and output type requirements of her program. Then when Bob's program is specified with T=15 May 2024, then his program no longer type checks when concatenated to the end of Alice's.
No one has yet written a system like this, but it would be really powerful if it did exist. Alice writes here smart contract conditions all by lonesome self, and Bob writes his. Then they literally concatenate one program to the other, and if it type checks then Alice and Bob can be certain that both sets of conditions are satisfied.
Bitcoin script is a large source of complexity, and it turns out to be mostly redundant. Schnorr signatures allow the use of so-called scriptless scripts [1] [2], which can do most of the things than Bitcoin script is used for, including multisig, absolute and relative timelocks, payment channels, discrete log contracts, and atomic swaps (using adaptor signatures). All without the need for a scripting language.
The example you gave of a multisig output that can be spent by either Alice, or Bob after some time, is easily handled too.
That's a stretch. Replacing timelocks with hashcash (or equivalent) is hardly the same thing.
But generally speaking "scriptless scripts" suffer from the need for interactive construction. There's a long way to go until scriptless scripts is a full replacement for script, if it is even possible.
Who said anything about replacing timelocks with hashcash?
I'm talking about actual relative timelocks, that put a minimum block distance between 2 particular transactions.
> suffer from the need for interactive construction.
Interactive construction is already widely in use in relative timelocks' prime application of payment channels.
The scope of potential smart contract applications is much broader, and vastly more interesting than payment channels (yawn). And payment channels are pretty much the only application (definitionally) in which you can get away with "all parties are online, or this contract will be cancelled anyway" assumptions.
Do you have a citation for a block-based relative timelock? The only such things I've seen are verifiable delay functions, which are a lot more like hashcash.
What about absolute lock times? Those are far more interesting in applications of business logic, like logistics contracts. Most of which require non-interactive state updates.
Not really, no. Lightning is still payments, multi-party and multi-hop. If the entire realm of Blockchain and smart contract technology was restricted to just payments, well I suppose that would be something. But far short of the total revolution of societal structure that was promised. I personally wouldn’t care to work on it if that was the case. Lightning is an implementation of distributed payments. Smart contracts are an implementation of decentralized law.
Your link to the mailing list thread describes essentially the same approach that bitcoin has for dealing with lock times. I would not normally describe this as “scriptless scripts,” which I have understood to me using the signing operation itself to achieve some goal that would otherwise be done in script. The locktime here is still enforced by special cased code of the consensus algorithm. If the number of things you want to do are fixed and enumerable then I suppose this is a valid approach. But it does not allow for general, arbitrary, future-defined constraints.
To give a concrete, simple example: show me how to do a return peg validation on scriptless scripts. If it can’t even do that, it is not a replacement for scripts.
The manual way. Validate SPV inclusion proofs using CAT, hash opcodes, bignum addition, etc. To be practical it requires block header commitments, but there are other reasons for wanting that. You also need relative locktime, which original bitcoin did not have. But that should be all that is required to be added. Other commonly cited things like Merkle branch verification opcodes just make the script more compact, or get around the fact that some required opcodes were later disabled and/or restricted from use with bignums.
Re: bitcoin vs. ethereum, the bitcoin community pre-ethereum was very invested in the idea of decentralizing all the things. I remember: I was there and part of that history. But over time people interested in more than just payments or the bitcoin asset have left or switched to ethereum. Originally expressive smart contracting was very much in scope.
Verifying cumulative diff requires verifying possibly thousands of headers (all those between peg out and peg in), which is a completely impractical amount of witness data for one script.
Committing headers in Merkle tree form or skip lists allow for logarithmic reduction in that number, as was worked out in the (2014?) sidechains whitepaper. 10’s of headers would be doable.
Beyond requiring intrusive changes to Bitcoin like header commitments, and still needing dozen-KB scripts for pegs, it also limits properties of the sidechain. For instance, if the latter wants to use a memory-hard PoW like Cuckoo Cycle, I don't see how Bitcoin script (which cannot even loop) could verify a cycle in a pseudorandom graph.
I could argue that there’s no reason for any proof of work other than sha256 as these side chains should be merge mining, but we’re way off in a tangent thread.
The point is that smart contracts actually do something other than “authorize payment”, and fancy Schnorr signing modes don’t come close to replicating those capabilities.
And so long as there is a need for a programmable verification architecture, Forth-like languages are prttty ideal.
Yes, I’ve long advocated for a high level smart contracting language that would be similar to prolog in structure and semantics. It would compile down to a state machine, and then the state machine would be interpreted as a series of outputs (nodes on the state machine graph) and spending transactions (edges).
The actual spend condition language would be lower level, however, and Forth-like languages are a good fit for this part of the stack.
But that doesn't directly relate to the verifiability of milliForth itself. An extremely shortened code can be harder to verify, for example it may work as intended unless a very specific input is used to break out of its sandbox (so to say). Bootstrapping needs a short and readable enough seed for that reason, and I can't be entirely sure that it is indeed the case for milliForth.
The sneakiest possible program representable in n bytes is never less sneaky than the sneakiest possible program representable in n-1 bytes, assuming you can pad a program out with nops.
Technically I guess what you'd do is hand type in binary code to create a hex editor, then bootstrap this forth off that, by hand-typing it in.
If you include formal verification tools as part of the stack then you can verify the tools by eye, type them in, and use them to verify the function of the stack.
Admittedly Forth is tricky to do here, but something like lisp/scheme/wat can actually be proven out with say microkanren.
There is of course no benefit to this thing at all other than reclaiming the crown from those deviant lispers... well I suppose if you're making a your own computer from scratch like https://www.homebrewcpuring.org/ it might be a useful starting point.
