> Is there a codebase you think of as exemplary that I could learn from?
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}" };
so I can just quickly do e.g.
$ ffd nip
: NIP ( a b -- b ) SWAP DROP ;
$ ffd allocate-pages
: ALLOCATE-PAGES ( num-pages -- 0 0 | addr -1 )
I ought to set keywordprg in Vim to that too, then I could get it in-editor.
Of course, this doesn't work for builtins and control constructs -- perhaps someday I'll have the compiler put the pointer in SOURCE in the word header, and write a language server that looks through them.
> [...] 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/