Post #2668001

@mc@mathstodon.xyz I'm a bit torn on this. On the one hand I agree with others in this thread that, even in a formalization-oriented venue, I expect a paper to bring something new, either on the formalization side (a new approach, technique, tooling, etc) or the topic side (a new proof, new result...). But on the other hand, I believe that contributing to the body of formalised mathematics/CS, in the form of reusable library code is also valuable, even if it brings little new insight. I don't know how we should support such work, papers feel like the wrong currency, but sadly they're the academic credit...