Use Coq in Your Browser: The Js Coq Theorem Prover Online | Hacker News Reader

Use Coq in Your Browser: The Js Coq Theorem Prover Online

jscoq.github.io

220 pointslelf41 comments

I've not used Coq for some time but previously toyed around with ProofWeb [0] which is a web interface to server side Coq. This seems like a much better approach and highly active.

[0]: http://proofweb.cs.ru.nl/

Coq 8.11 is going to be interesting - they merged ltac2 into the main tree and working hard on better integration. Coq 8.10 will finally come with CoqIDE GTK 3 port.

As well as a new sort, SProp!

https://coq.github.io/doc/v8.10/refman/changes.html#version-...

I am familiar with the basics of coq. What does the new SProp sort do? I couldn't understand the docs.

Were you able to find this doc [0]? As best I understand it, a Prop P has as many inhabitants as there are proofs of P, whereas an SProp S has at most one inhabitant, according to whether it is true or not. All proofs of S are declared to be "the same". (Convertible is the word they use.)

[0] https://coq.github.io/doc/v8.10/refman/addendum/sprop.html

Right; indeed they have _definitionally_ at most one inhabitant. Swiping the following spec from the page you link:

  Definition irrelevance (A:SProp) (P:A -> Prop) (x:A) (v:P x) (y:A) : P y := v.

the point is that `irrelevance` consumes an inhabitant `v` of the Prop `P x` and is supposed to "return" an inhabitant of the Prop `P y`. A priori `P x` and `P y` are different types but since `x` and `y` are both inhabitants of a type whose sort is `SProp`, they are definitionally equal and so `v` is definitionally a valid inhabitant of `P y`. This justifies the implementation of `irrelevance` as `v`.

I can imagine some other illustrative examples but I think I'll wait till I've played with SProp to confirm I'm not barking up the wrong end of the stick.

This is great! It's not going to replace proof general + (evil mode) emacs for me, but this would be a great way to introduce people to Coq without worrying about installation.

What’s the purpose of automated theorem provers? Seems to take the fun out of proofs

Ensuring the proof is actually one

https://www.quantamagazine.org/in-computers-we-trust-2013022...

Thanks, I'd imagine an extremely small number of proofs could be verified this way

There are archives of formal proofs that are quite big, e.g. https://www.isa-afp.org/ for Isabelle, https://github.com/UniMath for Coq

Thanks! This is really fascinating for me, i had never heard of this way of doing proofs and I studied math in college

There's an important distinction (spectrum?) between automated theorem provers and proof assistants. Coq is a proof assistant, which means that any automation is there to try to help the programmer by clearing away the tedious parts and leaving only the creative, fun parts. At the end of the day, it's still a human writing a proof. Afterward, Coq ultimately verifies the proof's integrity, which is an easy mechanical operation.

While coq is an automated theorem prover, I've had a tremendous amount of fun working my way through Software Foundations[1]. The vast majority of the proofs are assembled "by hand", but with coq verifying steps. For someone like me who has a "late in life" fascination with mathematics, doing proofs using coq has been fantastic.

[1] https://softwarefoundations.cis.upenn.edu/

i've always wondered how web and functional programming interact. there's, for example TypeScript and Elm. These are not designed for mathematical proofs.

https://www.typescriptlang.org/ https://elm-lang.org/

You'd probably do it in the theorem prover extracting it to a language with a web framework or use a language with a web framework that are both easier to prove. Here's a few places to explore:

http://www.impredicative.com/ur/

https://wiki.haskell.org/Web/Frameworks

Note: You'd pick the purest of them probably.

Most work I've seen on web applications with formal focus used model checkers, though.

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.397....

https://www.iro.umontreal.ca/~sahraouh/papers/Forte2004.pdf

I'd love to see an explanation of the runtime state/evaluation process of a Coq proof.

Is it supposed to take so long to load coq base (~ 5min)?

All I did was Require Import List Omega. and I am now stuck in package loading.

EDIT: From Coq Require Import List Omega. works. Database for hints not loaded? Can't seem to get eauto to work

It all seems very fast for me. I also see no problems with hint databases... maybe check the JS console for errors?

Side effect of living in Australia when every neighbour is netflixing. I discovered my network was dropping out very frequently.

Does this mean we can have a TypeScript binding to Coq?

Sorry to be the 15 year old, but could they have not chosen a better name?

Preemptively yes ive read the history of the name, but i doubt they didn't know the homophone.

The puns write themselves: More. Coq in Your Browser

Came here for this comment. I thought the Internet was for productivity, not Coq!

> Preemptively yes ive read the history of the name, but i doubt they didn't know the homophone.

Oh, from what I've heard, on pretty good authority, it was far from an accident. Apparently the French meaning of 'bit' is part of the backstory.

As a Frenchman, can confirm that the French homonym to 'bit' is the english homonym to 'Coq' ;)

English “bit” is not pronounced like French “bite”.

The vowels in “bit” and “beat” (or “shit” and “sheet”, or “bitch” and “beach”, etc.), sound completely different to native English speakers. The latter is closer to French “bite”. The former does not exist in standard European French.

Flesh-toned and harkening the imagry of many a 7th-grader's favorite bathroom doodle... A bold choice of icon for a software named Coq.

At least we don’t have to worry about what we would call It for touch-based devices. No easy way to do those kind of jokes in good taste.

Do you blush when ordering coq au vin in a restaurant?

The French have, in my opinion, overall a much healthier approach to sexuality than say, the British or Americans and I think there's much we can learn from them.

I don't really think it matters what the origin of the name is any more. The NIPS ML conference changed its name to NeurIPS, Mozilla spent $15K getting rid of the word "slave" in its repos. I personally don't believe this phenomenon is about sexuality per se. It's more of a never ending battle to remove all (real or perceived) traumatizing words from professional use, in the interest of inclusivity.

In the name of inclusivity.

There was a huge outrage epidemic over the past decade. Video games journalism was in a very dark place for a while as one example. The drive by "code of conduct" assaults on Github projects as another. Mainstream news orgs cashing in on, and a whole new generation of blogger/vloggers riding a tide of outrage porn. Interesting times.

Was? In my opinion it's still going on; they've just gotten better at dogpiling anyone who calls attention to it.

Fair. I feel like some of the communities finally found their voice and their patience for extremism peaked a couple/few years back but.. I also went from consuming most games journalism to barely reading any, so perhaps I'm just not exposed to the drama anymore. Seem to be a lot less drama in the OSS/software world though.

John Cleese vs Extremism seems relevant: https://www.youtube.com/watch?v=HLNhPMQnWu4

Yeah, but the thing about drama is that for it to be drama there has to be someone saying "No, this behavior is not ok." Those voices have largely been silenced and the behavior proceeds apace.

Completely agree, this piece from another comment reads like it was taken straight out of Twitch chat: "From Coq Require Import List Omega"

I'm surprised to have seen this flagged and dead when it's generally one of the top comments on anything to do with CockroachDB (which I think is a very normal name in comparison).

I'd feel weird about suggesting a tool at work called "vaj" or "tits" too. Feels a little much like encouraging a "boy's club" clique-y kind of atmosphere.

The boys club aspect I think is very important, and I think this aspect of tech culture might get some attention, but for thet most part is dismissed.

Coq is not pronounced like the English word “cock”. It also has no sexual or vulgar connotation whatsoever, and is just the standard French word for “rooster”.

>Coq is not pronounced like the English word “cock”.

Maybe they should mimic Facebook's name pronunciation bio line design feature and mention that obviously because that's news to me and people I've known that used the tool.

Coq in French is pronounced more like “coke” than “cock”.

Reply on news.ycombinator.com