How do people decide whether to submit a formalized mathematics paper to AFM or JAR? I think the emphases of the venues are different, but in this case I think we could write a paper with either emphasis. Right now my algorithm is just "ask my Ph.D. students which kind of paper they would rather write"