To what extent are questions about proof assistants on-topic?
I see four main classes of questions:
- Modeling a problem in a formal setting; going from the object of study to the definitions and theorems.
- Proving theorems in a way that can be automated in the chosen formal setting.
- Writing a correct proof in the chosen logic; in other words, getting the proof assistant program to typecheck.
- 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.