22

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
  • 2
    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
    Nov 21 at 9:28
29

provers.stackexchange.com

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".

New contributor
ice1000 is a new contributor to this site. Take care in asking for clarification, commenting, and answering. Check out our Code of Conduct.
15
  • 3
    the shorter the better
    – Jörg
    Nov 22 at 9:53
  • 1
    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. Nov 22 at 15:21
  • 1
    Alternate explanation: we as the proof assistant users are the provers, and this is our community 😌
    – ionchy
    Nov 22 at 21:08
  • 1
    On second thought, Z3 calls itself Z3 Theorem Prover. Is Z3 on topic?
    – Bubbler
    Nov 22 at 21:51
  • 1
    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
    Nov 22 at 22:16
  • 2
    @GuyCoder please I don't want Unicode URLs
    – ice1000
    Nov 23 at 0:33
  • 4
    @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. Nov 23 at 4:12
  • @MarioCarneiro Could you add an answer to my question?
    – Bubbler
    Nov 23 at 5:10
  • 2
    -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
    Nov 23 at 5:26
  • 4
    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. Nov 23 at 7:18
  • I am reconsidering my vote on this answer (though it says it's locked in). The original proposal seemed like it was only for ITPs instead of also ATPs. Even though I agree with Andrej about inclusiveness and talking with the ATP community, the scope might be too broad then. See my answer here.
    – k4rtik
    Nov 23 at 14:41
  • 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
    Nov 24 at 3:51
  • 3
    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 StaffMod
    Nov 24 at 20:24
  • @Catija what would be the overlords' choice then?
    – ice1000
    Nov 24 at 20:24
  • @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
    Nov 25 at 7:08
16

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
  • 4
    +1. We mathematicians don't post to math-overflow. Nov 21 at 13:47
  • 2
    proofassistants is 15 characters. Can we make it shorter? Nov 22 at 15:23
  • 5
    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 StaffMod
    Nov 24 at 20:25
  • 1
    @Catija Great, now I have a target on my back. :-) I know you guys are working hard and the timing is one of the worst days of the year to start this, so thank you and the team for all the hard work!
    – Guy Coder
    Nov 24 at 20:29
13

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.

8
  • 4
    I think it's too ambiguous. Nov 21 at 13:44
  • 1
    What can it be confused with?
    – k4rtik
    Nov 21 at 13:57
  • 15
    QED is a phrase which existed for thousands of years before computers. This site is specifically about computer proofs, not proofs. Nov 21 at 14:09
  • 1
    I agree with Kevin. Sorry I have to give this a down vote.
    – Guy Coder
    Nov 21 at 14:30
  • That's fair, I see the shortcoming of this name!
    – k4rtik
    Nov 21 at 15:37
  • 3
    Quantum electrodynamics ?
    – Jörg
    Nov 22 at 9:55
  • 4
    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?
    – tophat
    Nov 22 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
    Nov 23 at 14:59
6

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.

6
  • 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). Nov 21 at 9:47
  • 2
    I type urls with my bare hands on a cellphone outside of browsers if they're short enough
    – ice1000
    Nov 21 at 13:35
  • 1
    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
    Nov 21 at 13:47
  • I like this name because it precisely conveys the subject and should be easy to find.
    – Cheery
    Nov 21 at 15:14
  • 1
    proof-assistants is 16 characters. A shorter URL - the shortest that still makes sense - would be nice. Nov 22 at 15:27
0

proof.stackexchange.com

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

New contributor
darque is a new contributor to this site. Take care in asking for clarification, commenting, and answering. Check out our Code of Conduct.
1
  • 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
    Nov 25 at 5:21
-1

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
New contributor
Eduardo Cardoso is a new contributor to this site. Take care in asking for clarification, commenting, and answering. Check out our Code of Conduct.
1
  • 3
    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
    Nov 24 at 22:30
-3

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

New contributor
Sam Nead is a new contributor to this site. Take care in asking for clarification, commenting, and answering. Check out our Code of Conduct.
6
  • 5
    Jokes as an answer no, thus a downvote. As a comment I would give them an upvote. :-)
    – Guy Coder
    Nov 21 at 23:33
  • I love sorry-overflow :D though not all proof assistants use sorry to indicate holes in a proof I think?
    – Bubbler
    Nov 22 at 4:38
  • "Stack Overflow" is itself a joke name, having borrowed the term for a kind of failure. "Sorry" is mild, in comparison.
    – prash
    Nov 22 at 13:27
  • "Contradiction-overflow"? "P-and-not-P-exchange"?
    – Sam Nead
    Nov 22 at 13:34
  • Sure, or the classical term, "ex falso". I'm all for funny names!
    – prash
    Nov 22 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
    Nov 23 at 3:29

You must log in to answer this question.

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