[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).