The formal verification aspect doesn't really have anything to do with Forth, but I do expect the multistack concatentive calculus to be much more ergonomic tha

The formal verification aspect doesn't really have anything to do with Forth, but I do expect the multistack concatentive calculus to be much more ergonomic than applicative languages for linearity, which will play an important role in formal verification. We'll have to see how it all plays out, though. But that's my goal. I'm not really interested in writing just another programming language. Even if I fail miserably, hopefully breaking the work up into small pieces and publishing as I go will at least inspire others with similar goals.