Questions tagged [discussion]
Use if the question you're asking is designed to reflect different opinions or best-practices on a particular topic, with the goal of reaching community consensus.
61
questions
5
votes
1
answer
26
views
Code Reviews on topic?
There are two related questions here:
Question 1: Reviewing proof scripts? I just formalized a type system in Coq (and I'm almost certain it is not "idiomatic Coq"), would it be appropriate ...
4
votes
0
answers
38
views
Renaming "extensional-equality" to "extensional-type-theory"
Is there any better suggestion or reasons against changing extensional-equality to extensional-type-theory? As Couchy suggests, the current tag is slightly ambiguous. If there is no objection, I think ...
6
votes
0
answers
38
views
Are questions about categorical logic on topic?
Are questions about categorical logic and the related category theory are on topic on this website? Categorical logic is strongly connected to type theory and the semantic of (many) proof assistants, ...
4
votes
0
answers
40
views
How to write a tag wiki excerpt?
I'm hoping to establish some sort of guideline for writing tag wiki excerpts (or usage guidance).
Examples of tag wiki excerpts I find usually fall into two categories. The first references the tag ...
3
votes
0
answers
28
views
Should I create tags for common components in proof assistant implementations?
I'm asking questions about certain type-checking phases of a proof assistant (conversion-check, elaboration, ...
4
votes
2
answers
53
views
How detailed should tags be?
I saw a tag coq-definition. Should there be $\forall l\in \text{ProofAssistants}, l\text{-definition}$ tag? Should there be like ...
14
votes
1
answer
160
views
2022 Community Moderator Election Results
Moderator election #1 on Proof Assistants has come to a close, the votes have been tallied, and the new moderators are:
They will be your initial pro-tem moderator team — please thank them for ...
10
votes
3
answers
467
views
Candidate changes in 2022 Moderator Election – review your ballot
TL;DR: There's been a change in the candidate list for the 2022 Moderator Election. If you've already voted, you should confirm your votes still accurately represent your preferences. Details follow.
...
4
votes
2
answers
113
views
How can the actual count of those eligible to vote be determined?
In the election chat room I gave a count of the number of users allowed to vote: 126 users. I did this by looking at the users page and just counting them by hand. It started a series of others ...
5
votes
0
answers
116
views
What is wrong with the question "Formalizations of unsolved problems"?
There are comments suggesting that the question Formalization of unsolved problems should be closed because it doesn't contain the big-list tag. I don't understand this. Am I missing something?
...
7
votes
0
answers
168
views
2022 Community Moderator Election
The 2022 Community Moderator Election is now underway!
Community moderator elections have three phases:
Nomination phase
Primary phase
Election phase
Most elections take between two and three weeks, ...
15
votes
0
answers
249
views
Leaving Private Beta & Initial Pro-Tem Moderator Election!
Congratulations! You've met the participation and engagement expectations for an active private beta site and will be going into public beta tomorrow!
As we’re getting ready to wrap up the private ...
2
votes
0
answers
86
views
Is there a post that compares major proof assistants?
Is there a post that compares major Proof Assistants and provides suggestions of when to use each one, e.g. comparing: Agda, Coq, Idris, Isabelle, and Lean? With suggestions
If not, can create a post?
2
votes
2
answers
68
views
How to get more daily views?
The weakest point on the Area 51 Site is our views. We need to get a lot more if the site wants to leave beta.
But, how can we do this? As it says:
Eventually, 90% of a site's traffic should come ...
6
votes
0
answers
81
views
Should we have a Citation Helper?
It looks like a great deal of questions so far are about theoretical aspects of proof assistants and the underlying type theories. The answers to these questions rely on academic papers and conference ...