5
$\begingroup$

There are two related questions here:

Question 1: Reviewing proof scripts? I just formalized a type system in Coq (and I'm almost certain it is not "idiomatic Coq"), would it be appropriate to ask for a "code review" of my short script here? I honestly do not know what's considered idiomatic (or "best practices") in Coq, and I'd like to learn them, while correcting my script.

Question 2: Reviewing implementations of proof assistants? I've been tinkering around with implementing proof assistants in Standard ML; ostensibly, "down the road", I may desire a code review of some of these toy models. Would this be a proper place for such requests, or should I go to Code Review?

$\endgroup$

1 Answer 1

Reset to default
1
$\begingroup$

IMO if they are asking for a specific reason (like is there a more clever way to refute this case or whatever) should make it on-topic. Putting a piece of code and asking for review (unless it's short enough to make the point clear) should not be on-topic.

$\endgroup$

You must log in to answer this question.

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