[romforth]

I have ported Forth to a dozen small microcontrollers and my experience writing much of the bootstrap code in Forth tells me that you are better off coding Forth in a "vertical" style (ie one word per line with stack picture comments), rather than the terse "horizontal" code of "everything on one line" that many of the folks using Forth (including @yosefk, the author) seem to prefer.

Given how close Forth is to assembly (seen from an implementer's point of view) it makes sense to write Forth in a "vertical" style which reflects the "vertical" style in which assembly code is written. This has the advantage that the "stack picture comments" on each line of code can stand in for Hoare triplets so that the code and its - I'll call it - "proof" can be written hand in hand at the same time.

This is how all of the Forth code that I've written in https://github.com/romforth/romforth is structured.

It does make the code appear less compact though so you are not going to win any code golf prizes.

[Lerc]

Is there any editor/IDE support for stack state visualisation?

A text display with an auto pretty printed view would serve people who like both code styles well.

A newline per stack reducing operation with the next line indented by stack depth would make it close to your style and could be quite automatic.

[cess11]

Adjacent rather than a Forth, but take a look at Factor.

https://factorcode.org/

[7thaccount]

Also 8th. I find the free version fun to play with as a modern desktop forth with built-in support for things like databases, odbc, json, matrices...etc. The commercial aspect won't be most people's cup of tea of course, but I still think it's neat and 8th is probably the most approachable way to write a desktop app with forth.

https://8th-dev.com/

https://8th-dev.com/manual.html

[romforth]

Something like an automated proof assistant to help annotate the stack while coding would be awesome, but I'm not aware of any.

These might be famous last words, but if switching between compile/interpret modes is ignored, I think it shouldn't be too hard to implement it though.

[nxobject]

I do that's the rub with any language that works with procedural macroexpansion: it's conceptually hard to make diagnostics correspond one-to-one with original syntax. I think it might be especially hard with Common Lisp-style reader macros (i.e. procedures triggered at the parsing stage when a character is read in the input stream).

[volemo]

We removed explicit arguments from the language so you can write comments with arguments after every function call. :D