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.
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.
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.)
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.
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.
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.
i've always wondered how web and functional programming interact. there's, for example TypeScript and Elm. These are not designed for mathematical proofs.
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:
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.
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.
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.
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.
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.
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.
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.
[0]: http://proofweb.cs.ru.nl/