Went to a talk Klaus Sutner gave about his pedagogical habits. J. J. Schaeffer kept asking these semi-hostile, blustery old-mathematician questions, as I suppose one might expect him to, but he seemed to be more pattern-matching against things he expected to be indignant about (and proceeding to voice his indignation) rather than actually contributing much to the discussion.
I found it slightly saddening, because the way he taught logic and proof back in the two semester hodge-podge of basic math topics called "math studies I" and "math studies II" was actually extremely effective, (for me at least) but not for the reasons he seemed to be arguing about. The scarcely-motivated steamroller way he taught the subject matter of the course --- linear algebra, analysis, group and field theory --- was mostly terrifically dull, which certainly could be improved by the things Klaus was talking about. Making the presentation more "visual" isn't necessarily the right thing to do, and Klaus did mention this; the proper generalization of "visualizing" mathematical structures and results is having several different representations of them.
Anyway, I got side-tracked from the original point I wanted to make: that I found it really helpful, when I was first learning what a careful proof in "ordinary mathematics" was, to think of the task of proving in a very operational way. Specifically the idea of the first-order quantifiers was a bit mysterious before I took math studies, and after, it was crystal-clear, at both the informal and formal level.
It was all explained in terms of what you can do when you know a proposition, and what you can do when you are obliged to prove one.
If you know ∀x.P(x), then you can plug in any c you want for x, and then you know P(c). When writing an english proof, you say, "Since we know ∀x.P(x), then in particular, P(c)".
If you need to show ∃x.P(x), then you can plus in any c you want for x, and continue, trying to prove P(c). When writing an english proof, you say, "...hence P(c). This is a witness for ∃x.P(x)."
If you know ∃x.P(x), then make sure x isn't mentioned anywhere else, and go on knowing that P(x). In an english proof, you say "Okay, I know there is some x that has this property P. Choose one such x." or, rather, let your adversary choose one for you.
If you need to show ∀x.P(x), then similarly make sure x isn't mentioned anywhere else, and go on trying to prove P(x). In the english proof, say "Let an arbitrary x be given." which is again given to you adversarily, and you go on and show that P holds for this arbitrary x.
This stuff is all so baken into my brain now --- it's just the sequent calculus rules for the quantifiers --- it's almost hard for me to even write the above two paragraphs, to think about how I would dictatorily instruct someone about making proofs, even without explaining why these rules make sense. But they constitute one of the two main concepts that I took away from that class. (The other is thinking of vectors and matrices in terms of abstract vector spaces) In an environment of so many people fretting about how to teach the undergrad math and CS majors how to write proofs, I wish I could vote somehow for teaching such a natural-languageified version of the sequent calculus.