Out of curiosity, is there any interest in the Forth community for a type-checked Forth?
Type-checking of course could mean a variety of things, but, for instance, any Forth-to-X compiler has to check at a minimum that all code paths alter the stack in the same manner - at least for your run-of-the-mill definitions.