Questions about compilation errors in Coq

Question

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

http://cstheory.stackexchange.com/questions/1807/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:

http://cstheory.stackexchange.com/questions/846/eliminating-cofix-in-coq-proof/872

Answer 1

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.

Answer 2

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.

Answer 3

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.

Answer 4

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.