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