4
$\begingroup$

This question was raised in the comments of this question about idiomatic ways to prove the associativity of append.

A Rosetta Stone style question would describe some kind of task in a prover-neutral way, and each answer would show a way of achieving it specific to each prover.

Pros:

  • Potentially useful
  • Fills gap in ecosystem

Cons:

  • Not really a question
$\endgroup$
5
  • 3
    $\begingroup$ A rosetta stone question can be interpreted as "How do I formalize X in each proof assistant?", which sounds like a valid question. I guess a collection of good rosetta stone questions would be a valuable resource for the entire PA community. The tasks should be selected carefully though; we don't want this site to be flooded with near-duplicate rosetta-stones that add little value to the collection. $\endgroup$
    – Bubbler
    Commented Feb 16, 2022 at 4:02
  • 1
    $\begingroup$ Bikeshedding: the name rosetta-stone doesn't help potential new users to immediately find it. We may want to create synonyms. $\endgroup$
    – Trebor Mod
    Commented Feb 16, 2022 at 5:57
  • $\begingroup$ @Trebor I think a better way is to include such information in a canonical introductory Q&A, or an FAQ post on meta. In the area of programming in general, Rosetta Code is a pretty well-known site that collects solutions for programming problems in as many languages as possible, so the name should be recognizable enough for newcomers with programming background. (though I understand that it may not be for those with math background but not programming) $\endgroup$
    – Bubbler
    Commented Feb 16, 2022 at 7:38
  • $\begingroup$ Rosetta Code is a pretty well-known site As much as I wish that were true in general, it seems to be true in cliques. One clique that does not know about Rosetta Code are new programmers. I would not be surprised if I have commented ~200 SO questions and noted the site Rosetta Code has the answer to the question. Sometimes exactly as asked. $\endgroup$
    – Guy Coder
    Commented Feb 16, 2022 at 8:33
  • $\begingroup$ @GuyCoder I agree with you, hence "recognizable enough for newcomers [to proof assistants] with programming background". $\endgroup$
    – Bubbler
    Commented Feb 16, 2022 at 23:12

2 Answers 2

Reset to default
5
$\begingroup$

Stack Exchange's official stance is that

Since Stack Overflow launched, we’ve been trying to explain that it’s not just a Q&A platform: it’s also a place where you can publish things that you’ve learned: recipes, FAQs, HOWTOs, walkthroughs, and even bits of product documentation, as long you format it as a question and answer.

So we can accumulate any kind of relevant information on this SE site, as long as we can format that information as Q&A. The important word here is "format" - the Q doesn't need to be an actual question; it just needs to be formatted as such.

As I already said in the comment, "How do I prove this statement in each proof assistant?" is a valid question in this format. And then the corresponding answers would be "You can write this in Lean", "You can write that in Coq", etc. So the Q&A format is not the limiting factor in my opinion.

But, I also partially agree with Guy Coder that an external website dedicated to such a collection of code examples might be a better solution. One reason is organization of information; Rosetta Code supports various features that help browsing and contributing to the site (albeit hacky at times, given that it runs on top of a wiki platform) such as

  • a list of all tasks in one page
  • a list of tasks solved/unsolved in each language
  • a system to propose new tasks/languages
  • a discussion "board" for each task, and a global one

SE doesn't support any of these. (Well, technically we can discuss stuff about rosetta-stone posts on this Meta, but it would be mixed with other site-wide discussion.)

$\endgroup$
3
  • $\begingroup$ That "official stance" is antiquated though, and many of the popular sites on SE (even and especially this one) do not follow this format. $\endgroup$
    – Nike Dattani
    Commented Feb 17, 2022 at 17:10
  • $\begingroup$ @NikeDattani Because they're broader, not because they're narrower. Even Code Golf and Puzzling still allow Q&As. $\endgroup$
    – wizzwizz4
    Commented Feb 22, 2022 at 17:01
  • $\begingroup$ I have no idea what wizzwizz4 is talking about. No one said "broader" or "narrower" anywhere in this entire thread. $\endgroup$
    – Nike Dattani
    Commented Feb 22, 2022 at 17:45
3
$\begingroup$

Should we (StackExchange ProofAssistants) allow Rosetta-Stone style questions?

My answer to that specific question is no.

For this variation of the question

Should there be a Rosetta Code repository for proofs done with different Proof Assistants or solvable by automated theorem provers and such? (You get the idea)

My answer would be yes.

The change is do to the fact that I don't think this StackExchange site is the best place to put such information. StackExchange wants information packaged into questions with answers. The information is not a question and an answer. The information is a template or pattern with working examples to follow.

So the next question would be

Would GitHub Pages work as a repository for Rosetta Code style proofs? Would something else be better?

Those are rhetorical questions to make a point for why the initial answer is no.

EDIT

In doing a quick search found this

RosettaGit isn't the only project which aims to document tasks in multiple languages. Other projects do exist. Here's a list. Feel free to update and add to it.

This is not meant to say that specifically GitHub Pages should be used but others are creating tasks in multiple languages sites outside of StackExchange.

$\endgroup$
1
  • $\begingroup$ An example of such a repository is the Effects Rosetta Stone, but it's (non-)supported by a smallish community, so it's not really alive (but neither is the real Rosetta Stone). $\endgroup$
    – Andrej Bauer
    Commented Feb 16, 2022 at 17:13

You must log in to answer this question.

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