9 ms·

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

220 points by lelf 7y ago

chewxy 7y ago
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
- jmgrosen 7y ago
  It all seems very fast for me. I also see no problems with hint databases... maybe check the JS console for errors?
  - chewxy 7y ago
    Side effect of living in Australia when every neighbour is netflixing. I discovered my network was dropping out very frequently.
NotAnEconomist 7y ago
Does this mean we can have a TypeScript binding to Coq?
wlkr 7y ago
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/ http://proofweb.cs.ru.nl/
spork12 7y ago
We could all use some more Coq in our life.
jnordwick 7y ago
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
- mensetmanusman 7y ago
  Came here for this comment. I thought the Internet was for productivity, not Coq!
  - tomc1985 7y ago
    What a shame that this is being downvoted. More puns! If we pun them to death maybe they won't pick such silly names again
- leoc 7y ago
  > 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.
  - valw 7y ago
    As a Frenchman, can confirm that the French homonym to 'bit' is the english homonym to 'Coq' ;)
    - umanwizard 7y ago
      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.
- ducktypegoose 7y ago
  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.
- seanmcdirmid 7y ago
  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.
xvilka 7y ago
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.
- ocfnash 7y ago
  As well as a new sort, SProp! https://coq.github.io/doc/v8.10/refman/changes.html#version-8-10 https://coq.github.io/doc/v8.10/refman/changes.html#version-...
  - jeremysalwen 7y ago
    I am familiar with the basics of coq. What does the new SProp sort do? I couldn't understand the docs.
    - cvoss 7y ago
      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 https://coq.github.io/doc/v8.10/refman/addendum/sprop.html
      - ocfnash 7y ago
        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.
Gajurgensen 7y ago
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.
mmmonkey21 7y ago
I can't load it, must be my Coq blocker...
wownice 7y ago
haha COCK!
imranq 7y ago
What’s the purpose of automated theorem provers? Seems to take the fun out of proofs
- brohee 7y ago
  Ensuring the proof is actually one https://www.quantamagazine.org/in-computers-we-trust-20130222/ https://www.quantamagazine.org/in-computers-we-trust-2013022...
  - imranq 7y ago
    Thanks, I'd imagine an extremely small number of proofs could be verified this way
    - brohee 7y ago
      There are archives of formal proofs that are quite big, e.g. https://www.isa-afp.org/ https://www.isa-afp.org/ for Isabelle, https://github.com/UniMath https://github.com/UniMath for Coq
      - imranq 7y ago
        Thanks! This is really fascinating for me, i had never heard of this way of doing proofs and I studied math in college
- cvoss 7y ago
  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.
- pliftkl 7y ago
  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/ https://softwarefoundations.cis.upenn.edu/
7373737373 7y ago
I'd love to see an explanation of the runtime state/evaluation process of a Coq proof.
mrcactu5 7y ago
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://www.typescriptlang.org/ https://elm-lang.org/ https://elm-lang.org/
- nickpsecurity 7y ago
  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/ http://www.impredicative.com/ur/ https://wiki.haskell.org/Web/Frameworks 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.742 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.397.... https://www.iro.umontreal.ca/~sahraouh/papers/Forte2004.pdf https://www.iro.umontreal.ca/~sahraouh/papers/Forte2004.pdf

220 points by lelf 7y ago

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

jmgrosen 7y ago
It all seems very fast for me. I also see no problems with hint databases... maybe check the JS console for errors?
- chewxy 7y ago
  Side effect of living in Australia when every neighbour is netflixing. I discovered my network was dropping out very frequently.

NotAnEconomist 7y ago

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

wlkr 7y ago

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/ http://proofweb.cs.ru.nl/

spork12 7y ago

We could all use some more Coq in our life.

jnordwick 7y ago

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

mensetmanusman 7y ago
Came here for this comment. I thought the Internet was for productivity, not Coq!
- tomc1985 7y ago
  What a shame that this is being downvoted. More puns! If we pun them to death maybe they won't pick such silly names again
leoc 7y ago
> 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.
- valw 7y ago
  As a Frenchman, can confirm that the French homonym to 'bit' is the english homonym to 'Coq' ;)
  - umanwizard 7y ago
    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.
ducktypegoose 7y ago
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.
seanmcdirmid 7y ago
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.

xvilka 7y ago

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.

ocfnash 7y ago
As well as a new sort, SProp! https://coq.github.io/doc/v8.10/refman/changes.html#version-8-10 https://coq.github.io/doc/v8.10/refman/changes.html#version-...
- jeremysalwen 7y ago
  I am familiar with the basics of coq. What does the new SProp sort do? I couldn't understand the docs.
  - cvoss 7y ago
    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 https://coq.github.io/doc/v8.10/refman/addendum/sprop.html
    - ocfnash 7y ago
      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.

Gajurgensen 7y ago

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.

mmmonkey21 7y ago

I can't load it, must be my Coq blocker...

wownice 7y ago

haha COCK!

imranq 7y ago

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

brohee 7y ago
Ensuring the proof is actually one https://www.quantamagazine.org/in-computers-we-trust-20130222/ https://www.quantamagazine.org/in-computers-we-trust-2013022...
- imranq 7y ago
  Thanks, I'd imagine an extremely small number of proofs could be verified this way
  - brohee 7y ago
    There are archives of formal proofs that are quite big, e.g. https://www.isa-afp.org/ https://www.isa-afp.org/ for Isabelle, https://github.com/UniMath https://github.com/UniMath for Coq
    - imranq 7y ago
      Thanks! This is really fascinating for me, i had never heard of this way of doing proofs and I studied math in college
cvoss 7y ago
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.
pliftkl 7y ago
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/ https://softwarefoundations.cis.upenn.edu/

7373737373 7y ago

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

mrcactu5 7y ago

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://www.typescriptlang.org/ https://elm-lang.org/ https://elm-lang.org/

nickpsecurity 7y ago
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/ http://www.impredicative.com/ur/ https://wiki.haskell.org/Web/Frameworks 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.742 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.397.... https://www.iro.umontreal.ca/~sahraouh/papers/Forte2004.pdf https://www.iro.umontreal.ca/~sahraouh/papers/Forte2004.pdf