[HN Gopher] milliForth
___________________________________________________________________
milliForth
Author : binarycrusader
Score : 212 points
Date : 2023-11-06 03:03 UTC (17 hours ago)
(HTM) web link (github.com)
(TXT) w3m dump (github.com)
| anotherhue wrote:
| I love projects like these, reminds me of the magic within the
| machine, as opposed to the normal cacophony of the world that
| comes via the machine.
| digitalsankhara wrote:
| I do like this reasoning. Magic within the machine for me was
| programming forth as part of my post grad (controlling and
| processing proton precession magnetometers) and the device was
| a Triangle Digital Services (now defunct as a viable company I
| think) TDS2020 forth SBC.
|
| Almost a zen like experience - you, the machine and your focus.
| No world.
| LordShredda wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| Beside bootstrapping, Forth works well on tiny MCUs.
| adastra22 wrote:
| 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.
| eternityforest wrote:
| Forth doesn't seem to do much to stop you from making
| mistakes, unless Bitcoin has added extra stuff.
|
| I don't use or study anything crypto related, so I'm just
| guessing, but wouldn't something like Prolog work for
| describing contracts?
| rebolek wrote:
| Things that make sense and crypto are two set for which
| there's very small intersection.
| tromp wrote:
| 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.
|
| [1] https://github.com/BlockstreamResearch/scriptless-
| scripts
|
| [2] https://tlu.tarilabs.com/cryptography/introduction-
| to-script...
| adastra22 wrote:
| > absolute and relative timelocks
|
| 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.
| tromp wrote:
| 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.
| adastra22 wrote:
| 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.
| tromp wrote:
| > payment channels (yawn)
|
| 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.
| adastra22 wrote:
| 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.
| tromp wrote:
| > far short of the total revolution of societal structure
| that was promised.
|
| 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?
| adastra22 wrote:
| 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.
| tromp wrote:
| > But that should be all that is required to be added.
|
| 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) ?
| adastra22 wrote:
| You can add and compare bignums in bitcoin script.
| lifthrasiir wrote:
| 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 wrote:
| 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 wrote:
| You don't need a sneaky program, you only need a program
| that misbehaves on sneaky inputs.
| alexisread wrote:
| 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 wrote:
| 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/ it might be a useful starting
| point.
| benj111 wrote:
| : - not 1 + + ;
|
| Disclaimer: I've never written forth, so this may not be valid
| for any particular forth implementation.
| lynx23 wrote:
| Porting JonesFORTH to x86-64 was one of the most rewarding fun-
| project experiences lately. Forth is fun to play with.
| tromp wrote:
| > However, milliFORTH appears to be the smallest programming
| language implementation ever, beating out sectorLISP2, a mind-
| blowing 436 byte implementation of LISP, by 14 bytes.
|
| The sectorlambda implementation of Binary Lambda Calculus is
| shorter yet at 383 bytes [1].
|
| And the BLC self-interpreter is only 29 bytes [2].
|
| > A FORTH in 422 bytes -- the smallest real programming language
| ever, as of yet.
|
| That may still be true, as BLC is an esoteric programming
| language.
|
| [1] https://justine.lol/lambda/
|
| [2] https://ioccc.org/2012/tromp/hint.html
| eichin wrote:
| Hmm, I'd be a little surprised if this was smaller than some of
| the 8-bit era forths (the TIL book had a 50ish-byte "inner
| interpreter" for Z80 but that didn't include any of the
| baseline "words" that this does.) I'm sure it wins for 32-bit
| systems though.
| RodgerTheGreat wrote:
| The main advantage of a miniature Forth like this over BLC,
| Lisp, Brainfuck, etc, is that Forth grants low-level access to
| the hardware; you can easily bootstrap from it to something
| indistinguishable from a feature-rich Forth with a full suite
| of metaprogramming capabilities, or implement an entire
| operating system on top of it.
| mepian wrote:
| Nothing is stopping Lisp from having low-level access to
| hardware.
| tromp wrote:
| Is low-level hardware access part of the language definition
| [1] ?
|
| [1] https://forth-standard.org/standard/words ?
| jlokier wrote:
| Miniature Lisps are similar to Forth in this way. Having
| worked with both I'm inclined to favour Lisps for providing
| cleaner structure and abstractions for code and data to build
| up from, with low overhead despite the superfical
| differences. (See SectorLisp2 (436 bytes) vs SectorForth (491
| bytes) size: https://justine.lol/sectorlisp2/).
|
| Lisps are given low-level hardware access primitives
| (peek/poke etc) when they are designed for bootstrapping an
| OS, and low-level OS primitives (such as system calls) when
| they are designed for bootstrapping a rich environment on a
| different OS. Basically the same primitives as Forth for the
| same purposes.
| fuzzballcat wrote:
| Author here! I was trying to be very careful about making sure
| to phrase things in a way that was clear I was referring to
| "real" languages (ones that are used for actual production
| purposes), but inevitably I forgot to do so where you've
| highlighted. I've updated the wording so it's more clear.
| mikewarot wrote:
| I've always wondered how to boot a virtual machine from a single
| sector with no other OS... now I know, which is cool.
| badcppdev wrote:
| Does anyone in the Forth community know if Charles Moore is still
| with us?
| Stratoscope wrote:
| https://en.wikipedia.org/wiki/Charles_H._Moore
| tromp wrote:
| Still going strong at 85 years old...
| thesuperbigfrog wrote:
| He has recently done some amazing low power work with
| GreenArrays:
|
| "GreenArrays is shipping its 144-core asynchronous chip that
| needs little energy (7 pJ/inst). Idle cores use no power (100
| nW). Active ones (4 mW) run fast (666 Mips), then wait for
| communication (idle).
|
| Tight coding to minimize instructions executed will minimize
| power. The programmer can also reduce instruction fetches,
| transistor switching and duty cycle."
|
| https://youtu.be/0PclgBd6_Zs
|
| It is like the elegance of Forth in low power, multi-core
| hardware.
| badcppdev wrote:
| I think you're right that he's still at Green Arrays. Still a
| director there apparently.
|
| I do have to note that the linked video is from 2013 so I
| assume they've moved on from that.
| LeonenTheDK wrote:
| I have heard nothing new out of Green Arrays but the site
| still seems to be selling the boards. If I had free cash
| available I'd try ordering one just to see. It's a really
| interesting concept and I'd love to see it developed.
| weinzierl wrote:
| Yes, and so is Elizabeth Rather.
| t-3 wrote:
| He is. SVFIG's annual "Forth Day" meeting is on November 18th
| and he's likely to be there giving the traditional "Fireside
| Chat".
| badcppdev wrote:
| That's awesome to know. I remember reading his blog years ago
| when he was setting up Green Arrays
| alexisread wrote:
| Looking at the code, this looks remarkably similar to
| sectorforth? Thing is, with sectorforth and this, 2 of the
| primitives are not required so reducing the VM to 6ops, so you
| can probably go smaller. Looks as though Cesar was happy with
| fitting into a sector:
| https://github.com/cesarblum/sectorforth/issues
| fuzzballcat wrote:
| [Author here.] Indeed, sectorFORTH (as I have mentioned) was
| the primary inspiration and guide for this project! Ironically,
| in some places I even had a rather different design which
| converged on a more sectorFORTH-like design - it's really well
| put together.
|
| I've removed some primitives further from milliFORTH, but I
| haven't touched the arithmetic base. I hadn't seen those issues
| on sectorFORTH though, very interesting - I will look into it!
| alexisread wrote:
| Ah yes apologies, that'll teach me to look at the code before
| the readme!
| PaulHoule wrote:
| When I was in high school I wrote a nice FORTH for the TRS-80
| Color Computer using the OS-9 operating system which was a Unix-
| like multitasking OS that would fit on a 6809 microcomputer.
|
| I think it was around 2000 lines of assembly code to implement
| most of the FORTH-83 standard although mine was unusual in that
| it did not support the block-based I/O that was common on
| "language system" FORTHs but instead it had handle-based API for
| accessing files similar to Unix, C and MS-DOS in version 2 and
| up.
|
| The programming environment was a lot like Linux overall in that
| I'd use an ed or vi clone to edit files, then run something like
| an assembler or C compiler. I'd run my FORTH binary and it would
| present an interactive environment like most FORTHs.
___________________________________________________________________
(page generated 2023-11-06 21:00 UTC)