6 ms·

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

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.

gavinhoward 3y ago
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.
- eternityforest 3y ago
  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!
  - defrost 3y ago
    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>
    - AlotOfReading 3y ago
      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.
  - nine_k 3y ago
    Beside bootstrapping, Forth works well on tiny MCUs.
  - adastra22 3y ago
    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.
  - TerrifiedMouse 3y ago
    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.
- lifthrasiir 3y ago
  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.
  - taneq 3y ago
    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.
    - lifthrasiir 3y ago
      You don't need a sneaky program, you only need a program that misbehaves on sneaky inputs.
      - taneq 3y ago
        Those are the sneakiest programs.
  - alexisread 3y ago
    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. From there we can trust the software stack.
Avshalom 3y ago
subtraction is trivial to add in userspace once you've loaded it though : - 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/ https://www.homebrewcpuring.org/ it might be a useful starting point.
benj111 3y ago
: - not 1 + + ; Disclaimer: I've never written forth, so this may not be valid for any particular forth implementation.

gavinhoward 3y ago

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.

eternityforest 3y ago
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!
- defrost 3y ago
  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>
  - AlotOfReading 3y ago
    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.
- nine_k 3y ago
  Beside bootstrapping, Forth works well on tiny MCUs.
- adastra22 3y ago
  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.
- TerrifiedMouse 3y ago
  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.
lifthrasiir 3y ago
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.
- taneq 3y ago
  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.
  - lifthrasiir 3y ago
    You don't need a sneaky program, you only need a program that misbehaves on sneaky inputs.
    - taneq 3y ago
      Those are the sneakiest programs.
- alexisread 3y ago
  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. From there we can trust the software stack.

Avshalom 3y ago

subtraction is trivial to add in userspace once you've loaded it though : - 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/ https://www.homebrewcpuring.org/ it might be a useful starting point.

benj111 3y ago

: - not 1 + + ; Disclaimer: I've never written forth, so this may not be valid for any particular forth implementation.