7
$\begingroup$

To what extent are questions about proof assistants on-topic?

I see four main classes of questions:

  1. Modeling a problem in a formal setting; going from the object of study to the definitions and theorems.
  2. Proving theorems in a way that can be automated in the chosen formal setting.
  3. Writing a correct proof in the chosen logic; in other words, getting the proof assistant program to typecheck.
  4. Tool usage such as extracting code.

I think 1 and 2 are firmly on-topic here, 4 is firmly off-topic, and I wonder where to set the line with respect to 3. I've asked a test question which I think is close to the border. On which side?

Elsewhere on Stack Exchange: CSTheory has traditionally accepted these questions, but I get the feeling that part of the reason is the perceived lack of a better place. On the other side, there are coq questions on Stack Overflow, I don't know about other proof assistants.

$\endgroup$
4
  • 2
    $\begingroup$ I agree with your assessment. I think the same rules as for programming apply: questions that are useful no matter what proof assisstant I use are good, too specific ones are bad. $\endgroup$
    – Raphael
    Commented Mar 7, 2012 at 17:47
  • $\begingroup$ There is also the option to close too specific questions as "too localized": "This question is unlikely to ever help any future visitors; it is only relevant to a small geographic area, a specific moment in time, or an extraordinarily narrow situation that is not generally applicable to the worldwide audience of the internet." so we may not need to make them off-topic as a category. $\endgroup$
    – Kaveh
    Commented Mar 7, 2012 at 19:35
  • 1
    $\begingroup$ Aren't "test questions" explicitly discouraged for young betas? $\endgroup$
    – bitmask
    Commented Mar 7, 2012 at 21:09
  • 1
    $\begingroup$ @bitmask No, on the contrary, now is the ideal time. What's discouraged is artificial questions; my question is absolutely not artificial (I struggled with that a few years ago, and I think there's an answer on the Internet but spread over several Coq mailing list posts, so it's worth having somewhere, on SO if not here). $\endgroup$
    – Gilles 'SO- stop being evil'
    Commented Mar 7, 2012 at 21:23

3 Answers 3

Reset to default
3
$\begingroup$

There are two parts in the question the way I asked it: why the naive attempt doesn't work, and what can make it work.

What can make it work is a generic Coq programming principle. Seen this way, it's a job for Stack Overflow. But simultaneously it is a generic principle to prove something in Coq, which is a job for computer science. I could understand considering that part to be off-topic, but it's not clear-cut.

Why it doesn't work is a question about the theory behind Coq (the calculus of inductive constructions) or about one of the most subtle matters in the way Coq implements said calculus. This is definitely computer science, not programming.

$\endgroup$
2
  • $\begingroup$ I doubt that redirecting Coq questions to Stack Overflow is worthwhile. I imagine they'd be very likely to get bounced back here or to CSTheory. $\endgroup$
    – David Richerby
    Commented Nov 12, 2014 at 18:47
  • $\begingroup$ @DavidRicherby No, Coq questions do pretty well on SO. $\endgroup$
    – Gilles 'SO- stop being evil' Mod
    Commented Nov 12, 2014 at 19:46
2
$\begingroup$

I answered the test question and my answer is technical. Implementation details are indeed not exactly what I expect to be on-topic.

However answers about proof assistants are often borderline between deep theory problems and technical details, so I guess giving obvious rules about whether a question it is on-topic or boring stuff is hard. I guess the threshold would be if the question is only about programming (current Stack Overflow's Coq section is about that).

This would suit exactly in a Coq stack exchange site with both theory and practice questions, but that won't come out soon, so I find CS good for theory and SO for other questions.

So I guess Gilles's question would be in CS and my answer would be in SO...

$\endgroup$
1
$\begingroup$

About your test question: Because it's fair to assume that logical inconsistencies might be the reason hidden behind the provided error message, I think that the question is targeted at the theory behind coq and not at it's gory implementation details. Which makes it on-topic.

Also, I guess we could find on-topic and off-topic questions belonging to any of four points you mentioned. I think the “line” should be placed somewhere between Usage questions and Comprehension questions (closer to Comprehension), subjective to whatever area of CS is focused.

$\endgroup$

You must log in to answer this question.

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