Shachar Itzhaky (May 08 2022 at 12:02): Shachar Itzhaky (May 08 2022 at 12:02):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.
Karl Palmskog (May 08 2022 at 12:58):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?
Karl Palmskog (May 08 2022 at 13:01):I really like the improvements (typesetting, links, etc.) to the original submission I did of the sqrt2 example, well done
Michael Soegtrop (May 08 2022 at 13:01):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).
Michael Soegtrop (May 08 2022 at 13:02):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".
Michael Soegtrop (May 08 2022 at 13:03):If you rework the landing page, I would make this more obvious.
Michael Soegtrop (May 08 2022 at 13:07):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".
Karl Palmskog (May 08 2022 at 13:11):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)
Shachar Itzhaky (May 08 2022 at 17:37):@Michael Soegtrop Good point about agree about the scratchpad though.
Shachar Itzhaky (May 08 2022 at 17:38):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.
Emilio Jesús Gallego Arias (May 09 2022 at 15:02):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!
Emilio Jesús Gallego Arias (May 09 2022 at 15:02):Not to say 99% of the matematicians know a different version of this proof (using classical logic)
Emilio Jesús Gallego Arias (May 09 2022 at 15:03):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.
Emilio Jesús Gallego Arias (May 09 2022 at 15:04):I agree that the infinitude of primes was not a good thing for the landing page, but this is even worse.
Emilio Jesús Gallego Arias (May 09 2022 at 15:05):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
Emilio Jesús Gallego Arias (May 09 2022 at 15:05):So it is very misleading to point users to a set of tactics and libraries that are just not usable.
Emilio Jesús Gallego Arias (May 09 2022 at 15:05):Imagine lean landing page for math pointing to Lean's stdlib instead of mathlib
Emilio Jesús Gallego Arias (May 09 2022 at 15:08):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
Emilio Jesús Gallego Arias (May 09 2022 at 15:08):VST
Karl Palmskog (May 09 2022 at 15:08):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)
Emilio Jesús Gallego Arias (May 09 2022 at 15:08):@Karl Palmskog I agree
Emilio Jesús Gallego Arias (May 09 2022 at 15:08):it should not be the goal
Emilio Jesús Gallego Arias (May 09 2022 at 15:09):I don't know what the landing page should have, but this proof doesn't belong there, but in the examples dir, as a very specific, non standard proof
Emilio Jesús Gallego Arias (May 09 2022 at 15:10):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
Emilio Jesús Gallego Arias (May 09 2022 at 15:13):stuff such as all: auto are really not best practices and produce pretty slow and fragile scripts
Emilio Jesús Gallego Arias (May 09 2022 at 15:13):the page itself looks great tho!
Karl Palmskog (May 09 2022 at 15:13):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
Karl Palmskog (May 09 2022 at 15:15):my view is that it's probably better to pick flashy jsCoq stuff as entry, and then point to various "library" case studies
Hanneli Tavante (May 09 2022 at 15:15):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
Emilio Jesús Gallego Arias (May 09 2022 at 15:16):Yes, I think landing should be more of an index
Emilio Jesús Gallego Arias (May 09 2022 at 15:16):and target indeed different audiences! verification people will use a very different style than math people
Emilio Jesús Gallego Arias (May 09 2022 at 15:17):I don't think anyone is upset
Emilio Jesús Gallego Arias (May 09 2022 at 15:17):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
Emilio Jesús Gallego Arias (May 09 2022 at 15:18):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.
Emilio Jesús Gallego Arias (May 09 2022 at 15:18):and uses excluded middle
Shachar Itzhaky (May 09 2022 at 18:23):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.
Shachar Itzhaky (May 09 2022 at 18:26):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.
Shachar Itzhaky (May 09 2022 at 18:30):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.
Karl Palmskog (May 09 2022 at 18:31):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
Karl Palmskog (May 09 2022 at 18:34):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)
Shachar Itzhaky (May 09 2022 at 18:34):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.
Shachar Itzhaky (May 09 2022 at 18:36):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.
Karl Palmskog (May 09 2022 at 18:38):but maybe have a "jsCoq showcase idea" issue in the repo? Or is there one already?
Hanneli Tavante (May 09 2022 at 18:38):+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)
Shachar Itzhaky (May 10 2022 at 19:58):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).
Shachar Itzhaky (May 10 2022 at 19:59):We should definitely continue the discussion vis-à-vis a more thorough example portfolio.
Last updated: Jun 10 2023 at 06:31 UTC