0

Proposal: Proof Assistants

EDIT

In the comments below from an SE staff member it is noted

anyone can create tags on a whim in the private beta

which was nice to learn.

AFAIK the Private Beta last about 7 days. Based on this post during the private beta only 1 rep point is needed. However when the Public Beta phase starts 150 rep is needed which many should have but not all. So if you have low rep don't be surprised if you loose the privilege to create tags if/when the site transitions from Private Beta to Public Beta. :-)

As many know tags are useful and necessary.

One set of obvious starting tags is one for each of the Proof Assistants. These should be further clarified with version numbers and/or what ever means is used to indicate breaking changes, e.g. for StackOverflow C# has tags for C#, c#-2.0 ... c#-10.0 and even some variations for version 7, c#-7.1 ... c#-7.3

While I think there should be some basic starting tags I don't think it should be a free-for-all of creating tags. As the list of questions grows based on the user base the tags needed should be self-evident.

What other tags would be good at the start for the site Proof Assistants?

5
  • Deciding tags can tough before the site is fully. We were dissuaded from discussing possible site tags until our site actually went into Beta.
    – Tyberius
    Nov 21, 2021 at 13:59
  • @Tyberius In older days and for sites that would take months to make it into beta I would agree. At the rate this site is moving it might meet the requirements for beta in several more hours. Also this site has quite a few moderators committed, about half of those committed are seasoned SE users and those that use proof assistants have been around for a few decades so I would say the tags are well known. :-)
    – Guy Coder
    Nov 21, 2021 at 14:04
  • our site went into Beta a year and a half ago. If it were to go into Beta that soon (which seems unlikely, they usually take at least a week from full commitment to launching the private Beta) that would arguably be even more incentive to just have that discussion on your new Meta. I don't next think it's a bad idea to have this tag discussion early, I'm just pointing out how it was received on Area51 for us not that long ago.
    – Tyberius
    Nov 21, 2021 at 14:12
  • @Tyberius I get you, I really do and your looking out and taking an interest in this site is a good thing. I don't know how much you know about those committing here but it reads like a Who's Who. The group is very eclectic ranging from novices to world class experts, backgrounds in Math, Type Theory, Artificial Intelligence, Programming, Problem Solving and so on. Take some time to Google some of the names you see and you might be surprised!
    – Guy Coder
    Nov 21, 2021 at 14:21
  • 2
    This isn't a productive thing to be discussing here on Area 51 Discussions. Tags cannot exist without questions, and anyone can create tags on a whim in the private beta. No matter how much effort you put into this activity now, you are going to have more specific discussions in the beta phase on which tags should be removed because they were unnecessary or which ones should be more refined. Right now, you're just creating lists for no reason though.
    – animuson StaffMod
    Nov 21, 2021 at 16:01

2 Answers 2

Reset to default
1

Probably type-theory and set-theory?

1

Some ideas:

  • Tags for commonly used libraries, e.g. lean-mathlib, agda-stdlib, agda-cubical, UniMath, coq-HoTT
  • Tags for theoretical foundations: type-theory, set-theory, HoTT, cubical, univalence
  • Tags for thematic topics of formalisation: algebra, category-theory, topology, etc... (Also for non-math topics/applications, but I know little about those)

Not the answer you're looking for? Browse other questions tagged .