I was wondering if a "teaching" stream about teaching Coq or teaching with Coq would be a good idea.

Would it be interesting to some people?

This does sound like a good idea as this may encourage people to share stuff that they wouldn't have talked about otherwise.

Furthermore, there was a recent workshop on teaching (with) proof assistants, so this shows a general interest for this topic.

If there is sufficient interest, "teaching [with] Coq" should be a good name, thank you @Théo Zimmermann for the suggestion.

At the moment it does not seem to attract many people, but I created the stream anyway, in the hope that there will be more users after. Since we are going to have **the best discussions ever** it is bound to happen.

It is called "Teaching [with] Coq".

I arrive after the fact but I would have strongly preferred that the name starts with the string `"Coq"`

Cyril Cohen said:

I arrive after the fact but I would have strongly preferred that the name starts with the string

`"Coq"`

Why?

Because the streams are sorted in alphabetical order?

Then you can "pin stream to top".

Kazuhiko Sakaguchi said:

Because the streams are sorted in alphabetical order?

Yes, and thus "Coq teaching" would appear next to "Coq users" (and other "Coq ..." streams).

Théo Winterhalter said:

Then you can "pin stream to top".

Pinned streams are also sorted alphabetically among themselves :grinning: and it does not solve the problem of visibility of the stream for new users browsing the list.

It may be useful to advertise this stream here (and other places too).

PRs welcome :smile:

There is already a nice page about teaching Coq, accessible from the `Learning about Coq`

box in Coq home page.

It may be nice to create a box `Learning [with] Coq`

with a small text (like the draft below) and a pointer to `CoqInTheClassroom`

for more details ?

The teaching [with] Coq Zulip stream is a forum dedicated to various aspects of teaching Coq and use Coq as a tool for teaching various domains which would benefit from the possibility of building formal proofs (such as, but not limited to mathematics or formal methods in computer science).

This is a place where subscribers will share information about course outlines, libraries of examples and exercises, how to make these libraries available to the students, etc.

The wiki page is directly editable, feel free to add the link and your description there if that's what you had in mind.

And then maybe the page itself could be linked from `coq.inria.fr/documentation`

.

Last updated: Jun 23 2024 at 04:03 UTC