Re: Some user feedback

TLA+ is not so different from real-world programming languages: we
write (abstract) programs, then we compile/typecheck them, we run
them, we debug them. The workflow for TLA+ should be similar to, say,
Haskell. GHC has a compiler, a REPL, and a few command-line tools. It
does not have an isolated IDE; nor does it need one. Even tools like
Coq or Isabelle, which have their own little IDEs for interactive
proof assistants, are usually used via other generic IDEs like
Emacs.

The IDE is not exactly isolated. It is a specialization of Eclipse.

And somebody one day may want to make a package for tlaplus in emacs.

And my experience is that when you suggest somebody to learn emacs he looks at you as if

you wanted to come back to the stone age. I disagree with that obviously but is there a way of

convincing somebody in a democracy?