For example, this question: https://cs.stackexchange.com/questions/22864/lambda-calculus-difference-between-contexts-and-evaluation-contexts had two very thorough research-level answers, and was migrated to CS.SE.
I'm partly at fault with this, since I tend to suggest migration for theory B questions about $\lambda$-calculus which I believe to be simple/well-known.
I agree we should strive to be easier on these questions though: there's not much theory B going on at undergraduate levels, and there aren't many high-profile open questions, so there are a number of motivated, and "non-cranky" amateurs (or at least not researchers in those fields) out there, with few resources to learn.
Of course there are some "are these terms $\alpha$-equal?" questions, but for anything above that, I think we should be more tolerant of $\lambda$-calculus and Logic and Computation-style questions.
That said, specific questions about programing in Coq or Agda (or other ITPs) should be off-topic here and at CS.se.