I am still reluctant to promote (accurately quantifiable by both qualitative and quantitative methods XD) inferior proving styles in the front page XD but indeed we should move from the current landing structure.

now that you mention it Shachar we have been discussing about why math-comp is not accesbile and lean (which is very very similar is), now that the 10th anniversary of the feit thomsom proof is gonna happen

but that's a topic for a different thread, the landing page, I agree, should be very different

@Emilio Jesús Gallego Arias "inferior proving style" is ill-defined. Inferior for what purpose is the question.

@Théo Zimmermann as I mentioned, in the talk I didn't have time to give at the hackathon

I have proposed both a qualitative and quantitative criteria, but I will still do this seminar soon

it is not ill-defined in my case, you may agree or not, that's a different story

I guess people don't grasp how gigantic the proofs of 4 color and FT are

there are 5 lines lemmas in FT that contain more maths that full ITP papers

My point is that SSReflect/MathComp style can be considered superior for X, while being just inferior for Y.

in terms of proof difficulty,

sure I will discuss that, feel free to move this discussion to the proper topic and we can schedule my talk actually

actually I could use a lot of your feedback I'm sure

Emilio Jesús Gallego Arias: there are 5 lines lemmas in FT that contain more maths that full ITP papers

That's precisely the problem, we don't want to teach that to beginners

Most feedback I've had has been from interns that I taught

I agree math-comp is not accesible

but still, I can't teach my students a style that I know is not the one I prefer

but let's move this to the right place please

I agree with @Shachar Itzhaky about the landing page, I'm sure we can find a nice proposal that makes everyone happy

"That's precisely the problem, we don't want to teach that to beginners" Lean is doing that and see how Lean vs Coq for the mathematicians is working

The reality is that Coq for maths sucks, unless you use math-comp

and math-comp is not accessible

still works

10 years after, FT remain state-of-the-art

and papers written in 2009 could have been written today

so for sure I'm interested in fixing the accessibilty problem

? Lean people are precisely not using a mathcomp style?

Possibly unpopular (?) suggestion: What about a simple example (just as in the Lean tutorial) such as commutativity of addition? Then have links for other functionalities

pretty close to it

I think properties of lists is pretty canonical for Coq and does not need math-comp (it is not real math heh)

Emilio Jesús Gallego Arias said:

"That's precisely the problem, we don't want to teach that to beginners" Lean is doing that and see how Lean vs Coq for the mathematicians is working

Lean arrives years after Coq, teaches to beginners, uses an accessible style, and builds in just a couple of years a library that surpasses the size of MathComp (but according to @Cyril Cohen, this is not going to scale).

Indeed, because first thing is that IMVHO, people don't grasp the complexity of the FT proof, so many design chocies that happned in math-comp are actually there for strong reasons!

where math-comp failed is in being too focused on qed

and other factors

political problems were also a strong factor

that led to Coq to lose (co) leadership in the field of formal math

you can't do a project of that scale and just worry about the QED

but that's somethign we have learnt

I do agree that this is my own very personal view

but I have been programming from a long time

and I never liked when I was exposed to style that I thought bad when learning a new system

that made me lose interest instantly

a proof of the infinitude of primes that takes 200 lines?

I immediately don't want to learn more about that language

not for me

as a programmer I enjoy, even as a beginner, being impressed

with stuff that makes me wonder "wow how the hell they are doing that, looks crazy"

like when 25 years ago I saw haskell

I guess that makes sense, but I don't know how universal this is.

Yeah that's why I'm giving the talk

to get feedback, etc...

Especially if we are looking to expand our reach *beyond* hackers.

I could of course be very wrong

For mathematicians I only have a sample size of 2 (direct)

but once they got it, they were enjoying it quite well

and surprised

Opinion: A single example hardly works for everyone, I think. As discussed somewhere https://coq.zulipchat.com/#narrow/stream/314095-Coq-Hackathon.20and.20Working.20Group.2C.20Winter.202022/topic/Coq.20wiki.20getting.20started.20section , wouldn't it be more effective to have different examples according to the audience?

both interns

Hanneli Tavante said:

Opinion: A single example hardly works for everyone, I think. As discussed somewhere https://coq.zulipchat.com/#narrow/stream/314095-Coq-Hackathon.20and.20Working.20Group.2C.20Winter.202022/topic/Coq.20wiki.20getting.20started.20section , wouldn't it be more effective to have different examples according to the audience?

yes @Hanneli Tavante , I think that's the idea

the landing page should be more like an index page

Also, some other thoughts:

Who is going to see this landing page?

- If you are visiting the page and you never used Coq, how can you make a distinction between what is good and bad style? (Isn't it subjective too? This is a hard question...)
- If you are a total beginner, you probably want to get a general sense of what you can do with Coq
- If you are an exp. user who needs a quick space to try out some proofs, you might have your own standards.

Emilio Jesús Gallego Arias said:

but once they got it, they were enjoying it quite well

everybody seems worried about the syntax, but let me ask you all folks, where's Coq's Kevin Buzzard?

_nowhere to be found_

Hanneli Tavante said:

Also, some other thoughts:

Who is going to see this landing page?

- If you are visiting the page and you never used Coq, how can you make a distinction between what is good and bad style? (Isn't it subjective too? This is a hard question...)
- If you are a total beginner, you probably want to get a general sense of what you can do with Coq
- If you are an exp. user who needs a quick space to try out some proofs, you might have your own standards.

That sounds very good Hanneli, please add it to the wiki under the "Landing page session" entry

I wanted to develop my own example page, mixing rich text, images, Coq excerpts. Is there a quick route to this? I did not find an edit button on the landing page that would allow me to edit just this page and save it at a place of my choice.

Yves for now you need to use coqdoc, or write html by hand

What you want is planned and hopefully to land in time for the Coq workshop submission

If someone would like to help hacking I could actually guide them in the implementation, myself I got no hacking time until the 17th

but then I got lots, finally!

It reminds me that we have to take another look at Alectryon as a doc system that supports markdown together with Coq-related features; this can be useful for literate document editing as well as the jsCoq wiki.

Indeed I hope to chat to @Clément Pit-Claudel tomorrow a bit

maybe you would like to join?

Nice!! I do have some time tomorrow. What time?

Clément said 5pm , I proposed 6pm

both work for me so 5 pm is also good

tho I prefer later if possible

Paris time, I'm talking about

5p Paris is good for me as well. I can also do later. Let me know.

Great

I've sent a mail, we can sync offline

Last updated: Jan 31 2023 at 09:01 UTC