4
$\begingroup$

I would have voted to close the following question as out of scope if it didn't have 3 votes already.

How to define a function inductively on two arguments in Coq?

It is similar to asking how to write a function in a programming language like C++, or getting help about a compilation error. I think it is clearly out of scope for cstheory, as it is not a research level question in theoretical computer science, also it is too narrow.

ps: Almost the same considerations apply to the following question:

Eliminating cofix in Coq proof

$\endgroup$
6
  • $\begingroup$ Did you mean to link to a question instead of an answer in the second link? $\endgroup$
    – Tsuyoshi Ito
    Commented Sep 30, 2010 at 12:48
  • $\begingroup$ +1 for raising this issue. I never thought them as “programming questions” until I saw this. I am not complete sure whether the questions are off topic, though. $\endgroup$
    – Tsuyoshi Ito
    Commented Sep 30, 2010 at 13:03
  • $\begingroup$ @Tsuyoshi Ito: Yes, fixed, thanks. $\endgroup$
    – Kaveh
    Commented Sep 30, 2010 at 13:20
  • 1
    $\begingroup$ Do you know if such questions are fine on Stack Overflow? If such questions usually remain unsolved there because they are too theoretical, then maybe we should allow such questions. $\endgroup$
    – Robin Kothari
    Commented Sep 30, 2010 at 14:05
  • 5
    $\begingroup$ I doubt there would be many people who program Coq at StackOverflow.... I just checked. 8 Coq questions. $\endgroup$
    – Dave Clarke
    Commented Sep 30, 2010 at 14:07
  • $\begingroup$ It seems that people familiar with it think that it is a genuine tcs question. It is just difficult for me to distinguish between an on-topic theory of PL question and an off-topic programming/compiler error question. $\endgroup$
    – Kaveh
    Commented Oct 1, 2010 at 3:58

4 Answers 4

Reset to default
5
$\begingroup$

I don't know enough about Coq to tell the difference. I'm actually shocked that there's any discussion of this on SO :). From Yoichi's perspective, it might be good to cross post and link both posts to each other so the readers know what's going on, and so an answer might actually appear !

This seems like a genuine boundary case to me, but one where the OP has made a genuine effort to argue for relevance here (compared to some drive by questions that are way out of scope), and for that reason alone I'd support keeping it here. It got three votes, and some discussion, and that's good enough for me as a 'bottom-up' expression of interest.

$\endgroup$
10
$\begingroup$

When I posted my question, I believed it was about theoretical computer science. Now, I am eager to give information on this border case.

Whether the question is research-level or not

  • This question arose in a research activity in the course of verifying a well-known but error-prone algorithm.
  • I admit that an answer for this question will not make a research paper.

Whether the question is about theoretical computer science

  • I believe the following is a question about theoretical computer science: what kind of induction proofs are available in which formal theory (e.g. ZF with some axioms, type theories, or second-order arithmetics).
  • Coq is not merely a programming language, it is a type theory implementation that can be used to write theorems and proofs.

Whether the question is a programming question

  • The underlying purpose is showing correctness, not programming, but proving.
  • The question is about defining something, which is indistinguishable from programming in functional programming languages.
    • Those programming activity is necessary for proving something in a formal language.
$\endgroup$
0
8
$\begingroup$

This question is about proof assistants and verification tools. The level of knowledge required to use such tools is much higher than for regular programming. In some areas of TCS, such as type systems and other programming language theory, concurrency and verification, these tools are used extensively.

The fact that the question is described as being about compilation errors is misleading. The issue in the question is trying to find a particular monotonically decreasing measure function for the arguments of the Coq function being defined in order to prove that it terminates.

My argument is that such questions should be within the scope of what this site is about, of course depending upon the exact nature of the question.

$\endgroup$
1
  • 3
    $\begingroup$ "The issue in the question is trying to find a particular monotonically decreasing measure function for the arguments of the Coq function being defined in order to prove that it terminates." I'm not sure I buy that. Any CS freshman who learns Floyd-Hoare logic for proving imperative programs correct routinely has to come up with much subtler termination measures for homework. So if that's really his question then it's disqualified on other grounds. Anyway, my opinion is that aspects of Coq's metatheory (calculus of inductive constructions, etc) are on topic but not mundane programming issues. $\endgroup$
    – Per Vognsen
    Commented Sep 30, 2010 at 14:22
1
$\begingroup$

In his answer, supercooldave mentions “the exact nature of the question,” which I think is the very issue. The problem is: Is the exact nature of these questions “the theory of proof assistants and/or programming languages” or just “programming”?

  • If they are about the theory of proof assistants and/or programming languages and using Coq merely for concreteness, they are fine.
  • If they are about programming in Coq, they are off topic. The askers may want to ask them on Stack Overflow, considering there are several questions on Coq on Stack Overflow and they get some answers, although I do not know whether the answers are correct or not.

Honestly speaking, the more I think about it, the more the questions seem like programming questions.

$\endgroup$
2
  • 2
    $\begingroup$ A programming question can be on topic. Pfenning and Elliot: Higher-order Abstract Syntax (1988) (portal.acm.org/citation.cfm?id=54010&dl= ) is on how to use a proof assistant. I believe it is an important piece of theoretical computer science. $\endgroup$
    – yhirai
    Commented Sep 30, 2010 at 16:51
  • $\begingroup$ @yhirai , Tsuyoshi, in case if either of you hadn't seen this yet: Stack Exchange will very soon be launching a brand new site dedicated to computer-assisted proofs: please use my referral link here if you're considering to get an invitation to the Private Beta! I also posted on Meta about this. $\endgroup$
    – user1271772
    Commented Jan 16, 2022 at 4:48

You must log in to answer this question.

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