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.
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.
[1] https://github.com/BlockstreamResearch/scriptless-scripts
[2] https://tlu.tarilabs.com/cryptography/introduction-to-script...
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.
> suffer from the need for interactive construction.
Interactive construction is already widely in use in relative timelocks' prime application of payment channels.
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.
Don't you find 2nd layers like Lightning interesting, as a way to scale far beyond the limited L1 capacity?
> Do you have a citation for a block-based relative timelock?
See the thread starting with https://lists.launchpad.net/mimblewimble/msg00546.html
> What about absolute lock times?
Those are trivially supported in any Mimblewimble chain.
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.
Satoshi promised no such thing. That sounds more like an Ethereum promise (to which I don't subscribe).
> show me how to do a return peg validation on scriptless scripts
How does one do return peg validation in bitcoin script?
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.
If you're talking about SPV inclusion on another chain, wouldn't one also need to verify cumulative diff on that other chain (if PoW based) ?
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.
I don't use or study anything crypto related, so I'm just guessing, but wouldn't something like Prolog work for describing contracts?
The actual spend condition language would be lower level, however, and Forth-like languages are a good fit for this part of the stack.
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.
From there we can trust the software stack.
: - sp@ @ nand 1 + + ;
or as it appears in the hello_world.FORTH file : dup sp@ @ ;
: invert dup nand ;
: negate invert 1 + ;
: - negate + ;
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.Disclaimer: I've never written forth, so this may not be valid for any particular forth implementation.