33

Proposal: Proof Assistants

According to this answer, we do not really get to choose the name of the new site. Instead, the StackExchange overlords will create one for us. (They have had some negative experience with people quarreling over the naming of their site.)

As I understand things, unless there is good reason to deviate, they will pick proof-assistants.stackexchange.com. However, they occasionally deviate from the direct transliteration of the proposal name; for example, they shorten "computer science" to "CS" and such.

I propose that each answer to this question should start with the proposed name, followed by a rationale. As I said, this will likely all come to nothing, but perhaps a SE high priest is watching and will chime in. We're also going to see how civilized we are, as this is potentially worse than choosing the color of wallpapers with your spouse.

1
  • 3
    this is potentially worse than choosing the color of wallpapers with your spouse Oh but we do have to choose the wallpaper for this site. (ref) :-)
    – Guy Coder
    Commented Nov 21, 2021 at 9:28

10 Answers 10

Reset to default
42

provers.stackexchange.com

EDIT (3): I'm just proposing a domain name, not the name of the site. IMO, the site should be named as Proof Assistants.

It's much shorter than proofassistants, it's about proofs, it's easy to remember (just one word), and we rarely mean a non-computer one when we mention "prover".

EDIT: This word also unites automated provers and interactive provers, which according to the most voted answers to this question are both welcomed to the community. "Proof assistants" OTOH does not have such inclusiveness.

EDIT (2): a friend (Alex Chichigin) proposed verified.stackexchange.org which I think is cute.

20
  • 6
    the shorter the better
    – Jörg
    Commented Nov 22, 2021 at 9:53
  • 2
    I think @ice1000 is onto something here: short, easy to spell, easy to remember, no jargon, and more active/less passive than other proposed names. These criteria are vital.
    – Tim Carstens
    Commented Nov 22, 2021 at 15:21
  • 2
    Alternate explanation: we as the proof assistant users are the provers, and this is our community 😌
    – ionchy
    Commented Nov 22, 2021 at 21:08
  • 3
    On second thought, Z3 calls itself Z3 Theorem Prover. Is Z3 on topic?
    – Bubbler
    Commented Nov 22, 2021 at 21:51
  • 3
    If we want to only confine ourselves to proof assistants or interactive theorem provers, then this could be a concern. Z3 is one among several automated theorem provers. If we want to be broad and loose, then "prover" sounds good, but Z3 should be on-topic then.
    – k4rtik
    Commented Nov 22, 2021 at 22:16
  • 2
    @GuyCoder please I don't want Unicode URLs
    – ice1000
    Commented Nov 23, 2021 at 0:33
  • 5
    @k4rtik Automated theorem provers should definitely be on-topic here. I think we should not be stingy about scope, and allow anything related to formal methods, since these areas are all somewhat different in flavor from other CS and as the turnout should indicate there is a large refugee population that are used to being off topic everywhere else.
    – Mario Carneiro
    Commented Nov 23, 2021 at 4:12
  • 3
    -1. My main objection is that changing the name to provers would change the scope of the site to a site about formal methods
    – Couchy
    Commented Nov 23, 2021 at 5:26
  • 7
    I am in favor of this proposal, both because the name is good and short, and because it brings out an important point: we really could and should increase the scope to all kinds of "provers", whether they be interactive or automated.
    – Andrej Bauer
    Commented Nov 23, 2021 at 7:18
  • 1
    Upvote this comment if you have upvoted this but want to retract your vote now. (I was able to retract mine after the first edit, so I don't count here.)
    – Bubbler
    Commented Nov 24, 2021 at 3:51
  • 9
    Yeah... Im sorry, but we're very unlikely to use this - shorter names have to be inherent to the subject and (usually) unambiguous. "CS" as an abbreviation is because - in the computer world "CS" is frequently used for the purpose of shortening "Computer Science". The focus of this site seems to be on the assistants to the proving, and "provers" too easily is conflated with the humans rather than the computer programs - and... who knows... you might get spam about baking gear instead.
    – Catija
    Commented Nov 24, 2021 at 20:24
  • 1
    @Catija humans are not the assumed agents for the word "provers". Cf. Andrej Bauer's comment above on interactive and automated provers. For example, the Z3 theorem prover is not a proof assistant. The topic is further discussed here: area51.meta.stackexchange.com/questions/32621/…
    – prash
    Commented Nov 25, 2021 at 7:08
  • 5
    @Catija I see your point, but the alternative of using "proof-assistants" or "proofassistants" is worse, for so many reasons. There's already been discussions here about whether or not ATPs would be on-topic and not only proof assistants, and the overwhelming majority voted to include ATPs and higher-order theorem provers. I think it's dangerous to have the word "assistants" in the title since it will give the wrong idea. Maybe "Proof Assistants and Automated Provers" could be an alternative, but it's long and most people here will probably not vote for that.
    – Nike Dattani
    Commented Nov 30, 2021 at 20:11
  • 3
    @Catija I would argue that the term "provers" is both inherent to the subject (proof is in the name, although it is true that there are other uses of "proof" in e.g. baking but I guess they would not have sites dedicated to them), and mostly unambiguous. The fact that you could read "prover" as being either the human or the software seems like a strength to me; as a site we're interested in both sides of that equation. (But really, in the biz it always means the software, no one calls themselves a prover just like no one is called a "computer" these days.)
    – Mario Carneiro
    Commented Dec 9, 2021 at 17:14
  • 2
    That is, although it is somewhat jargon it is universally recognized in this field. "CS" seems similarly jargon, if we're making comparisons. It's a short abbreviation, so many things have those initials, but of course in CS everyone knows what CS means (for multiple values of CS).
    – Mario Carneiro
    Commented Dec 9, 2021 at 17:19
27

proofassistants.stackexchange.com

Notice there is no -

The reasoning behind removing the dash.

... some human users may have a difficult time recalling your domain name, especially because most people are used to domain names that don’t contain dashes

(ref)

However the keen eye will notice that I regularly use swi-prolog.discourse.group which has a dash. Go figure.

Anyway, now it is an option that can be voted on.

4
  • 8
    +1. We mathematicians don't post to math-overflow.
    – Kevin Buzzard
    Commented Nov 21, 2021 at 13:47
  • 6
    proofassistants is 15 characters. Can we make it shorter?
    – Tim Carstens
    Commented Nov 22, 2021 at 15:23
  • 8
    This is most likely what we would use for this site. It's simple and clear and unambiguous and it follows the pattern, which makes it easy to remember.
    – Catija
    Commented Nov 24, 2021 at 20:25
  • All done :) thanks
    – Nike Dattani
    Commented Jan 6, 2022 at 12:26
27

qed.stackexchange.com

It's short, it's quirky, it's about proofs, and it alludes to QED at Large: A Survey of Engineering of Formally Verified Software and the QED Manifesto.

7
  • 4
    I think it's too ambiguous.
    – Kevin Buzzard
    Commented Nov 21, 2021 at 13:44
  • 2
    What can it be confused with?
    – k4rtik
    Commented Nov 21, 2021 at 13:57
  • 19
    QED is a phrase which existed for thousands of years before computers. This site is specifically about computer proofs, not proofs.
    – Kevin Buzzard
    Commented Nov 21, 2021 at 14:09
  • That's fair, I see the shortcoming of this name!
    – k4rtik
    Commented Nov 21, 2021 at 15:37
  • 4
    Quantum electrodynamics ?
    – Jörg
    Commented Nov 22, 2021 at 9:55
  • 8
    I absolutely love this name! Admittedly, like Kevin said, QED is an older and more general term than the scope of the site, but so is "Stack Overflow". They give much of the same feel -- a jargon in-joke that still connects to the theme in question. After all, the primary purpose of a proof assistant is to help one to reach a QED and verify that "what was to be shown" was, in fact, shown. And, if you are like me and think proof assistants are future of formal logic, wouldn't it be great to tie the capstone of a proof (QED) to that concept?
    – tydeu
    Commented Nov 22, 2021 at 16:03
  • Thanks for the endorsement tophat, just to be clear I would still vote for this name (of course, self votes are not allowed).
    – k4rtik
    Commented Nov 23, 2021 at 14:59
7

proof-assistants.stackexchange.com

This is the default option, as I understand things. I am proposing it because it is self-explanatory and, well, default. The only disadvantage I see is that the name is a bit long. But who types URLs with their bare hands these days?

P.S. Once again, this entire exercise has a strictly advisory role. The SE site may choose whatever name they see fit.

7
  • 1
    I don't think hyphens are allowed so it may well be proofassistants.stackexchange.com. To me at least, the URL kind of looks like an online help service so it could attract spam when the site launches (but I guess it's inevitable as that is the known term).
    – TheSimpliFire
    Commented Nov 21, 2021 at 9:47
  • Of interest: Dash or Underscore in URL? Here’s How It’s Affecting Your SEO
    – Guy Coder
    Commented Nov 21, 2021 at 13:31
  • 3
    I type urls with my bare hands on a cellphone outside of browsers if they're short enough
    – ice1000
    Commented Nov 21, 2021 at 13:35
  • 2
    Of note: Using a hyphen in your URLs is recommended by Google, because it makes your website easy to read for humans. As an end result, this means that your site will place better on search engines. Also from Dash or Underscore in URL? Here’s How It’s Affecting Your SEO
    – Guy Coder
    Commented Nov 21, 2021 at 13:47
  • 1
    I like this name because it precisely conveys the subject and should be easy to find.
    – Cheery
    Commented Nov 21, 2021 at 15:14
  • 1
    proof-assistants is 16 characters. A shorter URL - the shortest that still makes sense - would be nice.
    – Tim Carstens
    Commented Nov 22, 2021 at 15:27
  • proof-assist is shorter.
    – Eduardo Cardoso
    Commented Dec 3, 2021 at 8:53
6

Theorem Provers

I love the suggestion by ErikMD of "Theorem Provers" if the company really doesn't allow "Provers".

  • Currently "Provers" has 43 upvotes and 6 downvotes, whereas "ProofAssistants" has only 30 upvotes and 7 downvotes.
  • Furthermore, consensus is not always about the sheer quantity of votes, but also the quality of the arguments for (or against) something, and the fact that there's clear consensus to make ATPs on-topic means that the name "ProofAssistants" (implying ITPs) would be too ostracizing to the ATPs community, so a more inclusive name, that better describes the userbase and what's on-topic, is necessary. "Provers" is one of the only proposed names with a high net score which accomplishes that task, but the company seems not to like that proposal for whatever reason.

In light of the above two points, "Theorem Provers" could be a fair alternative to "Provers" which is the proposal with the current highest net score (by a large margine). This would, among other things, completely take care of Catija's concern (though I don't believe it was shared by others) that we "might get spam about baking gear instead."

1

Formalized

Proofs have been there a long time, and such proof assistants and automated theorem provers help formalize them.

Using a verb past particle is similar to how the site Cross Validated does it (though its URL is stats.stackexchange.com). However, as what happens to Cross Validated, this might not be a good choice due to reasons mentioned in the link in the question. So I am just putting this here since no one mentioned it.

2
  • 1
    A verb, no. A verb is not something I would want the world to contemplate on what it means; there are too many nouns that could go with that verb.
    – Guy Coder
    Commented Dec 3, 2021 at 14:06
  • 1
    "Formalized" isn't unambiguous or exclusive/inherent to the subject of the site. See Catija's comment on ice1000's answer.
    – V2Blast
    Commented Dec 6, 2021 at 23:24
-1

Choosing a name for the Proof Assistants site

Name: Computational Logic

What is computational logic you ask, see: Computational logic: its origins and applications

Why that name? Because it catches most if not all of what others want to see included beyond just Proof Assistants.

Now (01/27/2022) many of the posted answers are giving a URL instead of a separate name.

For the URL

spock.stackexchange.com

Why this? Because it is catchy and I like Stark Trek until Paramount messed it up.

2
  • I am afraid this name, while historically correct, is a bit too arcane.
    – Andrej Bauer
    Commented Jan 27, 2022 at 15:17
  • @AndrejBauer Really, and thus proofs are not arcane.
    – Guy Coder
    Commented Jan 27, 2022 at 15:22
-2

mathproof.stackexchange.com

I believe in the strength of this name for being:

  • Easy to remember
  • It sounds good
  • Denotes authority on the topic
  • Connects directly to the target audience
  • Connects directly to the Function
1
  • 5
    The proof written in proof assistants isn't always math. Often you prove correctness or other guarantees about a computer program for example. And the name has very little connection to proof assistants.
    – Bubbler
    Commented Nov 24, 2021 at 22:30
-2

proof.stackexchange.com

It's a shorter alternative, and it doesn't imply that automated theorem provers are the main topic.

1
  • 5
    This would not happen. It is even more ambiguous than the "provers" suggestion above. Please read the staff comment there as to why this is unacceptable.
    – animuson StaffMod
    Commented Nov 25, 2021 at 5:21
-3

I think it important to get the joke suggestions out of the way early.

6
  • 6
    Jokes as an answer no, thus a downvote. As a comment I would give them an upvote. :-)
    – Guy Coder
    Commented Nov 21, 2021 at 23:33
  • I love sorry-overflow :D though not all proof assistants use sorry to indicate holes in a proof I think?
    – Bubbler
    Commented Nov 22, 2021 at 4:38
  • 1
    "Stack Overflow" is itself a joke name, having borrowed the term for a kind of failure. "Sorry" is mild, in comparison.
    – prash
    Commented Nov 22, 2021 at 13:27
  • "Contradiction-overflow"? "P-and-not-P-exchange"?
    – Sam Nead
    Commented Nov 22, 2021 at 13:34
  • Sure, or the classical term, "ex falso". I'm all for funny names!
    – prash
    Commented Nov 22, 2021 at 14:14
  • Speaking of failures, "proof-of-false" is probably the ultimate failure of proof assistants, though it might sound negative and it's three words long...
    – Bubbler
    Commented Nov 23, 2021 at 3:29

You must log in to answer this question.

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