I too, would personally prefer a command line REPL. But sometimes you are interested enough in a thing to try it out, but not interested enough to install things. Coq, in particular, is a pretty brutal installation process if you aren't already an emacs user. These web REPL's are great for reducing the friction necessary to try something out, and thereby getting people more interested. This one in particular is a big win for convenience over existing tooling.
I will add, I think it can be very disheartening for people who put a lot of their own time into making something happen and then having a random commenter say, 'Yeah, but I would rather have had something else, that wasn't at all the project you set out to make.'
> Coq, in particular, is a pretty brutal installation process if you aren't already an emacs user.
It's only "brutal" if you're compiling from source, in which case you've got to compile all of the ML and then all of the Coq libraries. That's only necessary for experimental branches though; I've not used an OS which doesn't provide binaries of official releases.
The installation process is basically "apt-get install coq && coqide", or whatever package manager your system uses. That will run the GTK interface which comes bundled with Coq.
The only time when Emacs might have anything to do with Coq is in relation to Proof General; but the only reason to run PG is if you're already an Emacs user. It's been in maintenance mode for years, and being rapidly overtaken by asynchronous interfaces based on PIDE (eg. the jEdit and Eclipse plugins).
I'm a very happy Emacs user, but just because I use Coq via PG doesn't mean I'd ask non-Emacs-users to do the same; in the same way that I access my GMail account via Gnus, but wouldn't try to convince non-Emacs GMail users to do the same.
I hear what you're saying, but that's the risk you must take when you do a public display like that. Besides, it's at least half the fun. What's the use of only fanboys (& -girls) commenting, if that's not the whole picture?
PSA: Names in software matter. I know we want to believe we live in some language agnostic utopia, but the fact is, programming culture, literature, and science, is dominated by the english language... so when you name your language something like "Coq" (sounds like cock), or Nimrod, (a common american childrens insult), or your OS, Losethos, (which has the word Lose in it, even though it is an actual place...), You face a tremendous barrier to adoption. Case in point, the previous examples, Nimrod changed their language name to Nim, and have seen a recent surge in visibility/popularity, Losethos renamed to TempleOS, and has seen a similar wave of attention... Names matter.
A real REPL (i.e. in your shell, not in your browser) that uses MathJax or whatever for result rendering would look much more interesting to me.
If the universe ever comes to an end it will be because it has been rewritten in JS.