Pre-submission enquiry - Are projects about proof assistants eligible?

[faenuccio]

I am wondering if works contributing to Math libraries for proof assistants like Isabelle/HOL and its library Archive of Formal Proofs; or like Coq and the library Mathematical Components; or Lean with Mathlib; and the likes, are eligible for publication and within the aims&scope of JOSS.

[danielskatz]

Can you explain what you are thinking of in terms of reasons this type of work might or might not fit?

[faenuccio]

Well, the point is that several papers in this field are still being published in a very "traditional" way, with a long-ish pdf explaining the math that is being formalised (a content that is seldom innovative, since most of formalisation works nowadays concern well-established mathematics), some code snippets, and a static link to a git repository. But the core of the work is the code, and this normally concerns something around 10k LOC (rough estimate). Just to cite some examples, one can have a look at https://doi.org/10.1007/s10817-021-09593-0 or https://doi.org/10.1007/s10817-022-09644-0 or https://doi.org/10.1007/s10817-022-09643-1 (I stop here, I have simply looked at the latest issues in one important journal). It is of course difficult, if one so wishes, to classify these works as being CS or Math (and it probably depends a lot on a paper-by-paper base), but they all share the property of mainly consisting of code, that is research-oriented, and being hosted on git repositories from the start.

I should probably make it clear that I am not trying to submit a paper now, I am writing as a member of the community who wishes to explore if JOSS is a reasonable option for people working in the field.

[danielskatz]

Some questions that we would ask (from https://joss.readthedocs.io/en/latest/submitting.html)

1. Are these software, licensed with an open-source initiative approved license?
2. Are they hosted at a location where users can open issues and propose code changes without manual approval of (or payment for) accounts (e.g, an open git repo, GitHub, etc.)?
3. Are they research software and do they have a research application (are they likely to be used by other researchers, and to be cited by them as key parts of their research)?
4. Are they research tools, not research results?
5. Was sufficient scholarly effort involved?

I'm not sure I can answer any of these, but if you think the answer is yes, the best thing might be for someone in the field to submit one, in part as a test that we can specifically examine.

I'm going to close this now, but feel free to reopen it if you think more discussion would be helpful.

[faenuccio]

Well, concerning the points 1, 2, 3, 5 the answer is "yes" and easily documented (for 1. there only exists one proof assistant, to my knowledge, that is not open-source, but this should only discriminate papers about that software, not all others proof assistants, I guess). Concerning 4, I would like more discussion to understand what the different between a research tool and not a research result is. Formalising a theorem will help other people formalise other theorems that rely on the first one (does it make it a tool?); but formalising even undergraduate level theorems can often be challenging, so achieving such a formalisation might be seen as a research result.

[danielskatz]

I'm not sure I can help in 4 in general. @olexandr-konovalov - do you have any thoughts on this?

[olexandr-konovalov]

@danielskatz @faenuccio I think that a system/framework/infrastructure for formalising theorems would be viewed as a research tool, while a formalisation of one of several specific theorems (achieved using the said research tool) would be viewed as a research result, even if formalising of that theorem would enable formalisation of further theorems.