My experience is that with a development methodology that emphasizes early-binding, incremental testing, and aggressive factoring, I just don't have the same kinds of memory issues I do in C. Strings having an explicit length helps a lot, and I suspect stack manipulation having a linear-types-like feeling helps somewhat too, since you think a lot more about "should this be removing this from the stack" than "should I be using this variable again some time, you know, later."
> because you're building a platform for safely running untrusted code written by players who are competing against one another, or because, given your own fallibility, you think it's the only way to be safe enough from ransomware gangs
My aarch64 Forth runs under QEMU, and this is easy to set up, and wiring a PL011 to stdio works great.
If you're just trying to avoid buffer overruns, though (which I suppose meets the latter case but not really the former), I'd consider using a 64-bit Forth with 32-bit pointers and 32-bit offsets, storing the size of the allocation in the first word before the pointer, so you can check the offset in a special TAGGED!/TAGGED@. I suspect you'd still want the normal !/@ for speed, and implement TAGGED!/TAGGED@ in terms of them, though?
Perhaps the MTE extensions would work, but I haven't investigated them (I don't have a laptop whose CPU that supports them yet).
Interesting! I definitely haven't reached that level—in Forth I have the same kinds of memory problems I have in C, and also parameter-passing bugs and type errors. Is there a codebase you think of as exemplary that I could learn from? Or, maybe better, a screencast of somebody writing some software in the development style? (Interactive testing of new words doesn't leave development artifacts, after all.)
"Much better than C" might still be pretty bad compared to JS, Rust, or OCaml; have you tried them?
> My aarch64 Forth runs under QEMU, and this is easy to set up, and wiring a [UART] to stdio works great.
This is definitely a viable approach that can work in many circumstances! However, each trust domain in QEMU uses 16 megabytes of RAM and roughly a million microseconds of CPU time to start up and shut down, and if you're doing cross-architecture emulation so you can't use kvm, the CPU overhead is typically on the order of 300%. By contrast, each trust domain in Lucet takes about 16 kilobytes of RAM and 50 microseconds of CPU time to start up and shut down https://www.fastly.com/blog/lucet-performance-and-lifecycle, and a new trust domain in a language that implements object-capability security could conceivably take 16 bytes of RAM and 0.1 microseconds. In both cases you can usually come within a few percent of native-code performance—which probably isn't in the cards if every memory access is preceded by a bounds check, as in Valgrind (typically 1000% CPU overhead) or this pseudo-Forth approach. Communications round-trip time might be 1 μs per ping-pong in QEMU and 0.1 μs in the other cases.
So, there are cases where a secure-compiler approach can give you 3–6 orders of magnitude better performance than just using QEMU. If you have a multiplayer game where each player uploads code, you might be able to support a few hundred players on a PC with the QEMU approach, or a few hundred thousand players with the Lucet approach. (Not, probably, all connected over TCP at once.)
> consider using a 64-bit Forth with 32-bit pointers and 32-bit offsets
An interesting idea here is to use a 64-bit system with 64-bit pointers and 32-bit offsets, mapping each allocation 4 gibibytes and change apart. Basically using the high 32 bits of the pointer as an MTE address tag or segment ID. Bloated and probably slow, though, and of course the bounds checking isn't very precise—enough to ensure that you can't index into another allocation, but not enough to catch every off-by-one array indexing bug.
There used to be a fat-pointer bounds-checking version of GCC that replaced pointers with essentially Golang slices, and you could of course implement that kind of scheme on top of a standard Forth, much as you suggest with TAGGED@.
My "one codebase I keep rewriting" is [0]; I don't consider the artifact as useful as the process, though. Particularly,
> in Forth I have the same kinds of memory problems I have in C, and also parameter-passing bugs and type errors.
I find the memory problems are helped a lot by incremental testing in the REPL, as well as designing in such a way that it's obvious what a word does -- if a word has a surprising side-effect or requirement, that's a good sign some design rethinking is in order. Thinking Forth [1] has some examples of the kinds of redesigns that can be helpful, though as a warning it has strong "grumpy old man" vibes. I find these hilarious, but some don't :) (Some of its design suggestions are also somewhat "off" in my view; not a huge fan of DOER/MAKE, personally.)
I definitely don't often experience parameter-passing bugs (assuming you mean "this takes 3 args, thought it took 2") nor type errors, and I'm actually a bit surprised to hear you do. I suppose I rather religiously stack comment, and write just about every word to have a "static" stack effect. I've also got a shell alias:
ffd() { rg -FiIN ": $1 (" "${2:-$HOME/Projects/stahl/kernel/src}" };
$ ffd nip
: NIP ( a b -- b ) SWAP DROP ;
$ ffd allocate-pages
: ALLOCATE-PAGES ( num-pages -- 0 0 | addr -1 )
> [...] JS, Rust, or OCaml; have you tried them?
Yeah, more the latter two than JS. Maintaining memory safety is easier in a memory-safe language, but I'm not certain overall correctness and design simplicity is. Certainly, when I'm implementing things in OCaml, I feel like I have to make design compromises much more than in Forth (where Forth gives me more room to redesign instead of getting forced into an unideal compromise). Rust's macros give me a bunch more leeway, but it's still occasionally awkward to express some things where something really is just easier to express at runtime, but it's impossible or UB/unsound to do so.
Common Lisp is perhaps a better competitor in this regard, since like Forth it supports both powerful compile-time and run-time metaprogramming. Maybe MetaOCaml too, though I've yet to try it.
> However, each trust domain in QEMU [...]
Yeah, of course QEMU isn't a silver bullet in this regard; if your application needs to be able to spawn large numbers of sandboxes quickly, especially. If you wanted to push virtualization as far as it could go, I'd consider the rust-vmm/Firecracker work instead -- they have stock Linux booting in 250ms/core, and a (perhaps custom) ringbuffer shared between the two processes would of course be vastly lower overhead than proper emulation of hardware.
> [...] Lucet [...]
I actually considered dropping WASM in initially, but I removed it after remembering my experience with trying to do JITtish things in it -- it's not currently practical (as of like a year ago) to do a DTC Forth, or a Forth that inlines, in WASM, since words are just too small. WASM being an "extreme" Harvard architecture is also fairly annoying. I suppose an ITC Forth ought to work, but without an inliner, performance seems like it'd be fairly bad.
I believe there's an API in spec-development currently to add better primitives for JIT that's sized closer to a basic block, so maybe that would change the situation.
> [...] object-capability security [...]
If you're going that... high-level? abstract? why not use Factor? I think, as you describe above, a Smalltalk-inspired approach might be a better foundation than most Forths' "assembly-inspired" ones. Though, as I understand it (too young to have lived through it!), Smalltalk had awful performance until Self came along and invented modern JIT, by which point you've completely lost the virtue of simplicity of implementation (at which point I'd be biased to say, you should use a Lisp or Haskell variant instead!)
> [...] 64-bit pointers [...]
Yeah, I considered a variation of that (most memory bugs are off-by-n for a small n, so guard pages are almost as good), but having a minimum allocation size of 4k seemed too wasteful.
> [...] replaced pointers [...]
Oh, I think TCC [2] still implements that! My understanding was that doing that relied on the sorts of C UB rules that some people hate (and that I quite like that Forth lacks!) though. I suppose if sizeof(uintptr_t) == 2*sizeof(ptrdiff_t), that wouldn't need to use the rules, but I think that'd suck pretty bad in Forth.
---
I think there are (at least!) two axes being compared here:
1. How easy is it to write correct Forth (I include security in correctness -- arbitrary code execution is typically pretty incorrect!)
2. How easy is it to execute attacker-provided Forth safely
I'd say Forth is strongly competitive on the first axis, and isn't at all on the second. I'd certainly believe that Factor or a Smalltalk-like Forth could be competitive on the latter, but if you include bugs in the compiler and runtime as correctness violations, I suspect it'd suffer a lot on the first axis.
I've thought a bit about getting stronger assurances of correctness for my Forth programs without complexifying the implementation of the system (which would make incorrectness much more likely). Currently I'm thinking about doing proofs in separation logic, with symbolic execution acting to hopefully provide a high degree of proof automation. An important characteristic is doing these proofs on the program starting at some physical machine state at a fixed time (e.g. just before some main loop is entered), rather than on the abstract machine that the runtime and compiler hopefully implement correctly. I think the system is simple enough that no mismatch between the two would occur, but I suppose I'll see whenever I've finished learning enough to start implementing this.
---
[0]: https://git.sr.ht/~remexre/stahl/tree/main/item/kernel/src [1]: https://managedway.dl.sourceforge.net/project/thinking-forth... [2]: https://bellard.org/tcc/
By "parameter-passing bugs" I mean things like "I forgot to put a DROP after this loop that was keeping a variable on the stack" or "this takes 3 args, and I knew that, but I accidentally passed it 2, and then it took me an annoyingly long time to figure it out".
I don't really think of Factor (or PostScript) as being terribly similar to Forth despite their concatenative syntaxes, although maybe that just means I'm emphasizing a different aspect of Forth than you are. I feel like Factor and PostScript are more like Lisp or (especially) Smalltalk than they are like Forth, just with less syntax.
The thing that appeals to me most strongly about Forth is the prospect of a steam-catapult-like leap from machine code, through a few hundred lines of code, to a fairly usable low-level programming language environment: concise code with nested expressions, recursive functions, named variables, ad-hoc compile-time metaprogramming, function pointers (DEFER or DOER/MAKE), a form of closures (CREATE DOES>), and an interactive REPL that doesn't need to be restarted to see code changes (though maybe not a single-stepping debugger). That is, it's the simplicity of the implementation that appeals to me, with the transparency and malleability that implies.
But I don't really prefer to type b negate discrim sqrt + 2 a * / instead of -b + sqrt(discrim()) / (2*a) or (/ (+ (- b) (sqrt (discrim))) (* 2 a)). I don't really like having to type "." or "?" to see the result of an expression I'm evaluating interactively. I don't think the RPN syntax is actually better, mostly, though it has some real advantages as a user interface. I just think the RPN syntax is an acceptable tradeoff for the simpler implementation, more powerful metaprogramming and refactorability, and better performance that the Forth design provides, and it's easy enough to use it to implement something more reasonable.
I'm still more intimidated than I should be by formal methods. I've found DRMacIver's QuickCheck-like Hypothesis, which randomly searches for counterexamples to your assertions of properties you would like your program to have and then reduces them to minimal test cases, to be astoundingly effective at improving my testing, and I've been thinking something like his "Minithesis" could be a significant boost to getting a new programming environment up and running. But that's about as far as I've gotten.
Ah, yeah, incremental development is the panacea here.
> [...] Factor (or PostScript) [...]
Yeah, agreed; if you're needing to be able to safely execute untrusted code though, I'd rather have a language with trustworthy properties (i.e. one restricting one from making arbitrary syscalls, arbitrary pointer reads+writes, etc.) rather than applying sandboxing to a language that allows the program to do all these unsafe operations.
> [...] leap from machine code [...]
Agreed :)
> [...] prefer to type [...]
Yeah, I haven't found a syntax for reading math that's better than infix; I don't actually think the postfix is much better than prefix, but maybe that's just me.
> [...] RPN syntax [...]
Oh, I actually think it does; it emphasizes function composition directly, and unifies it with sequencing statements in a single syntax!
> [...] formal methods [...]
Yeah, especially given the diversity of techniques under the formal methods banner, it's hard to get a good look at "the whole landscape." I think symbolic execution is getting to the point where it's workable for testing with a similar UX to property testing, just slower but with stronger guarantees (since all possible executions are taken, not just the ones that the RNG finds). Haven't actually built it yet though, so maybe Forth's flexibility will make it too hard, who knows.
If you wanna chat more about these things, I and at least one other person looking into formal methods + Forth hang out on #forth on Freenode.
That's a bit off-topic but I would say any interpreter for a dynamically typed language that use a GC. That is to say almost anything but Forth (at least in the non-AoT category)
> Well, precisely what I want is to be fail-fast; standard Forth pointer arithmetic isn't
That particular point is often addressed by "correct by design". If it is really important not to off-by-one, you can make your array a power of two in size, and then access it through "gate keeping" words that bitmask the index. Or perform a quick check on the passed index using the same technique.
This is of course not a one-size-fits-all solution, but one useful thing Forth taught me is to think about things in their context. Specialization leads to simplification, generalization often leads to complications.
> You say, "The paradigm in Forth is to increase the skills of the programmer," which is to say, to be more difficult than necessary.
If you want to jump higher, you train yourself to jump higher by raising the bar a little every day, you don't lower the bar a little every day and pretend you've improved.
When you train yourself you build the muscles involved in the task you are training for. Eventually what was next to impossible last month is easy today. It is not difficult anymore.
"Difficult" is not an absolute value.
> I mean, you're probably right that most people using Forth today are doing it, like Apollo, not because it is easy but because it is difficult.
I did not really say that. I have no idea of how many people are using Forth in production, as a hobby, as a personal tool or as a puzzle game.
> But that's not what Chuck Moore was looking for, it's not what Elizabeth Rather is looking for, and it's not what I'm looking for either.
Chuck Moore has been developing Forth for 50 years. When you say he is not trying to make Forth more difficult, you are right but you are IMHO mistaken on the means. One of his attempts was "source-less programming" [1]. It was a dead-end, but IIRC the experiment led to ColorForth.
E. Rather is retired now I believe, but what she was looking for as a co-founder of Forth, Inc. is to sell Forth. That's a different objective, and that led co-founder C. Moore to leave the company in order to pursue his personal vision of Forth.
For one thing Forth, Inc. has pushed ISO-Forth because a standard gives credibility and makes things a bit easier for their customers, but Moore was quite not favorable to the principle of an "executable" standard and criticized it for being too complicated.
Okay, but if you use, say, Lua instead of Forth, you're going from an interpreter that weighs 4 kilobytes to one that weighs 100 kilobytes. And instead of running 5 times slower than C (assuming a conventional threaded-code Forth), it runs 20 times slower (assuming not LuaJIT). And you've lost inline assembly. And you've lost compile-time metaprogramming (and if you want eval, which lets you get some of it back, the price goes up to 150 kilobytes). And you can no longer write real-time code because of the GC. And, even without real-time requirements, your programs randomly fail in limited-memory environments because they're allocating all the time, and sometimes they suffer atypical allocation fragmentation. And the memory requirements aren't just unpredictable, they're also large, because most of your memory is taken up by pointers, so even when your programs don't crash randomly in a low-memory environment they can't do as much as Forth.
There are other compact interpreted languages with other tradeoffs: BASIC, Smalltalk, XLISP, ZIL, Red, Elisp, and PostScript, for example. But they all have many or all of the above drawbacks.
So I don't think it's unreasonable to try to find a spot in the design space that's closer to Forth than it is to Lua and PostScript. GC and dynamic typing clearly aren't necessary for memory safety. The resulting language clearly wouldn't be the same thing as Forth, but that doesn't mean it has to have the kinds of orders-of-magnitude disadvantages listed above.
> If it is really important not to off-by-one, you can make your array a power of two in size, and then access it through "gate keeping" words that bitmask the index. Or perform a quick check on the passed index using the same technique.
This is going to the opposite extreme from "fail fast": unless the desired semantics is really an infinitely replicated buffer, like if you're using it as a ring buffer, this is deliberately producing incorrect results to mask the programming error of an out-of-bounds index. There are situations where that's a good idea (any possible way of handling such an error in an NPC script in a first-person shooter would be better than crashing the game, and ring-buffer FIFOs are a perfectly reasonable way to communicate with interrupt handlers and real-time threads) but there are also a lot of situations where failing fast is better.
> I have no idea of how many people are using Forth in production, as a hobby, as a personal tool or as a puzzle game.
My objection to your comment was basically that you seemed to be saying that anyone who's using Forth as something other than a puzzle game is doing it wrong.
Yes, doing things in a way that's more difficult than necessary is a worthwhile activity and makes you stronger. Football players get better at playing football by lifting weights. But they don't carry the weights with them onto the football field. That would make them worse at playing football.
> Specialization leads to simplification, generalization often leads to complications.
An important insight. You're right about the history of Forth, too.
1. What should you use if you want memory safety guarantees—whether because you're a novice, because you have better ways to spend your Saturday nights than disassembling core dumps, because you're building a platform for safely running untrusted code written by players who are competing against one another https://news.ycombinator.com/item?id=27160615, or because, given your own fallibility, you think it's the only way to be safe enough from ransomware gangs? Of course you're right that it's not ANS Forth or polyForth or machineForth, but what should it be? What's the lowest price in complexity we can get away with paying for that pearl? Surely we can do better than JavaScript. Or even PostScript.
2. You say the paradigm in Forth is "correct by design", "fail-fast" and to fight complexity uñas y rostro. Well, precisely what I want is to be fail-fast; standard Forth pointer arithmetic isn't, because indexing past the end of an array will just access some other object. That means that instead of failing fast it will usually produce incorrect results and possibly corrupt the data in that other object, producing errors downstream. To fail fast we need bounds-checking, and for bounds checking we need to distinguish pointers from integers.
3. You say, "The paradigm in Forth is to increase the skills of the programmer," which is to say, to be more difficult than necessary. You're free to make your Forth more difficult than necessary if you want, which is an enjoyable activity that will surely make you a better programmer, but that isn't what Forth was designed for. In fact it's close to the opposite of Forth's design principles, which are to fight complexity because complexity makes programming more difficult. That's why Forth programmers in the 01980s had IDEs with virtual memory, incremental recompilation, compile-time metaprogramming, reflection, and multithreading that fit on a floppy disk and could run in 64K of RAM. It's not because F-83 was written by superhumans; it's because Forth's design removed a lot of accidental complexity from the problems, allowing its implementors to focus on the essence.
I mean, you're probably right that most people using Forth today are doing it, like Apollo, not because it is easy but because it is difficult. But that's not what Chuck Moore was looking for, it's not what Elizabeth Rather is looking for, and it's not what I'm looking for either.