JsCoq | Hacker News Reader

JsCoq

github.com

107 pointscolinprince15 comments

But if I run Coq on the client anyway, why would I take a gratuitous detour through the browser?

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.

> If the universe ever comes to an end it will be because it has been rewritten in JS.

Insert joke about theories that the universe is a simulation here.

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.

By the way, there is also the OPAM package manager for Coq to install Coq and user libraries easily: http://coq-blog.clarus.me/use-opam-for-coq.html

...it can be very disheartening...

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?

This is 403 Forbidden at the moment, but if it's a way to run Coq in a browser, ProofWeb is also of interest:

http://prover.cs.ru.nl/login.php

Forbidden

You don't have permission to access /rhino-coq/ on this server.

https://github.com/ejgallego/jscoq

Thanks, we updated the link to GitHub for now.

> rhino-coq

At least the devs have a sense of humor.

wasn't the whole point of Functional Programming to avoid languages like JavaScript (or even OOP like Python, C++)?

No, not really. Lisp and other functional languages predate the articulation of OOP:

https://en.wikipedia.org/wiki/Functional_programming#History

http://userpage.fu-berlin.de/~ram/pub/pub_jf47ht81Ht/doc_kay...

So functional programming isn't a reaction to OOP.

It's also the case that Python is not particularly OOP (it does seem to me that lots of people that came to it from Java use it that way).

Original link FYI:

https://x80.org/rhino-coq/

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.

Reply on news.ycombinator.com