After some discussion among the community, and with very good suggestions from @Hanneli Tavante, we have a new and (hopefully) improved landing page. There is a preview at https://coq-p-wr.vercel.app/.

Notably, the mathcomp infinitude of primes example was moved to a separate page and the landing page now shows the proof that sqrt 2 is irrational, based on a development by @Karl Palmskog. We all agreed that while users should be made aware of the vast benefits of utilizing mathcomp, esp. for proofs involving numerical math, the more common denominator among users, with an emphasis of newcomers, is plain Coq types and tactics. Perhaps another page dedicated to "intro to mathcomp" is in order.

Let us know what you think.

I completely agree that MathComp deserves a jsCoq intro of some sort, maybe even split into basic SSReflect intro and bool/seq/fintype intro - maybe inspiration can be taken from MathComp book?

I really like the improvements (typesetting, links, etc.) to the original submission I did of the sqrt2 example, well done

Btw.: my younger son (now studying CS) tried JsCoq a while back, and it took him (and me) quite a while to figure out that one has to press the "open scratchpad" icon in order to write your own Coq file (rather than going through the tutorial).

We are both using quite a variety of SW on different OSes, so I don't think we both live in some sort of "UI bubble".

If you rework the landing page, I would make this more obvious.

My wife might have a different opinion on the question if I see obvious things, though. Usually when I ask here if she has seen this or that, the answer is "right in front of you".

my view of the long term solution to the Coq UI question: we should probably all be using AI-based assistants (that will automatically highlight UI elements and the like, when they are useful)

@Michael Soegtrop Good point about agree about the scratchpad though.

The section "Creating your own proof scripts" used to be higher up before the example. Now that it's lower, there should probably be a stronger cue for how to get there.

I'm afraid I think that this proof is not a very good publicity for Coq, specially among mathematicians. To start with, what's written in the text is not what's written in Coq!

Not to say 99% of the matematicians know a different version of this proof (using classical logic)

We should do a poll, but if I was a mathematician and saw this, I would be driven away from Coq, not attracted to it.

I agree that the infinitude of primes was not a good thing for the landing page, but this is even worse.

WRT math-comp vs not math-comp, there is not really a choice. Coq doesn't even have matrices in the standard library, much less groups or anything fancy beside a few aritmethic facts

So it is very misleading to point users to a set of tactics and libraries that are just not usable.

Imagine lean landing page for math pointing to Lean's stdlib instead of mathlib

There is a myth about a "plain" version of Coq existing. It just doesn't exist. As of today, there are at least 5 or 6 well developed version of Coq's tactics and libraries, including SF, Compcert, Arthur's CFML, IRis, math-copm

VST

should the goal of the landing page really be to draw in mathematicians? I don't think Lean has ever had much advertising there. If anything, something game-based could be used to draw people in (compare natural number game and friends)

@Karl Palmskog I agree

it should not be the goal

I don't know what the landing page should have, but this proof doesn't belong there, but in the examples dir

It is interesting how the point I tried to make with the original landing page (that people were doing the proof of the infinitudes of primes using 1000s of lines of tactics, whereas you only need 3) still stands 7 years later

stuff such as `all: auto`

are really not best practices and produce pretty slow and fragile scripts

the page itself looks great tho!

for additional changes, it may be good to decide first what the goal should be then, i.e., is it to showcase jsCoq itself or Coq itself or something else? As a showcase for Coq, I think the point of the infinite-primes proof is lost on most

my view is that it's probably better to pick flashy jsCoq stuff as entry, and then point to various "library" case studies

Idea: Now that there is a Navbar, we can have multiple examples targeting different audiences.

Maybe the landing page could hold something very simple, explicitly stating that "the example below illustrates how jsCoq works"

Also, it'd be good if the example on the landing page did not lead to any style discussions (not saying these discussions should not exist! But jsCoq landing page might not be the best place for them)

What about something like commutativity of addition? (Lean also uses it IIRC)

It does not seem to make anyone upset

Yes, I think landing should be more of an index

and target indeed different audiences! verification people will use a very different style than math people

I don't think anyone is upset

however we need to be careful with the image we give to non-expert, ITPs have a reputation for being not usable and that's for very good reasons

so taking a proof that 99% of mathematicians known and presenting it with a non standard proof style for Coq + maths, plus a very strange proof, doesn't seem the best idea for me. If we want sqrt of 2 let's do it classical way, which is pretty easy with math-comp analysis.

and uses excluded middle

I am somehow skeptical that a single page can draw in someone who is a mathematician and is completely unfamiliar with Coq. The target audience IMHO is people who have heard of Coq from their colleagues or from reading a paper and come in looking for a taste. I do agree, that the taste should not be bitter. I have no strong opinion about this proof vs. a more standard proof; I am totally in favor of encoding the standard classical-logic proof. Do we really need to pull in mathcomp as well? `Require Import Classical`

is available in vanilla Coq. But maybe what is most disturbing to the mathcomp people is that doing numerical stuff in vanilla Coq is just using the wrong tool for the job. Also, commutativity of `+`

is a bit boring (sorry Lean :sweat_smile: ), how about list stuff? A personal favorite of mine is `rev (rev l) = l`

. It is also not the most exciting theorem but the proof is elegant and easy to follow.

The `all:`

stuff is my fault, this was not in any of the existing versions of the proofs, and I agree that perhaps that should be discouraged; it does have some pedagogical advantages esp. relative to using `;`

because it is easier for the learner to observe intermediate state of the proof and exactly which subgoals were solved by the last tactic. For this purpose I usually prefer it in demonstrations, even if I would not include it in my actual developments.

Another point about showing off jsCoq itself: I liked the fact that reading the core of the proof with jsCoq is easy even without looking at the full proof. Esp., the user can click on the `comparison_`

lemmas and see their types, as well as the `Nat`

lemmas from stdlib. This is something that I would be happy if can be present in the revised example as well. But it is by no means a must.

there are only a few people in the world who can effectively use mathcomp-analysis at the moment. The CS equivalent might be to show off MetaCoq or CertiCoq, which similarly might belong to a research showcase, but are not good landing page material

if one wants to show off math in a flashy way, the verified function graph generation in CoRN or Coquelicot could also be nice (verified pixel placement)

I agree, I think we are accumulating a set of "benchmarks" that should be listed in the navbar and appeal to different audiences and this seems like a very good idea to have them. We also have Iris that has been getting a lot of traction and I was planning to include an example of SL properties from the POPL'21 tutorial there as well.

A model that I keep having in the back of my mind is the CodeMirror 5 webpage https://codemirror.net.

You visit the page and immediately see "This is CodeMirror" with the simplest instance of the editor embedded and fully functional. There is a nice selection of demos for a reader who looks for more.

but maybe have a "jsCoq showcase idea" issue in the repo? Or is there one already?

+1, maybe the goal of the landing page should be telling the reader what is jsCoq, and not focusing too much on the examples (we can add them in dedicated pages and link everything at the navbar)

Hi all, I have written the rev-rev example, and updated the preview page (https://coq-p-wr.vercel.app/). You are welcome to add more suggestions in the PR (https://github.com/jscoq/jscoq/pull/268).

We should definitely continue the discussion vis-à-vis a more thorough example portfolio.

Last updated: Jan 30 2023 at 17:03 UTC