This is a tough question, because we should be sending students looking for reasons and explanations, rather than proofs alone. I know this is a loaded statement, but different proofs of a result highlight different aspects of the same fact, and constitute different parts of the explanation of that fact.
If this were not the case, we wouldn't value multiple proofs of a given theorem.
That said, a student you should be sensitized to what is routinelike approach 2, and what is not. The parts of even a proof that are automated and standard little, you should not use up a major portion of the student's time. Herein lies the value check out chapter 3 of"proof training". A nice book for this,
How to Prove It: A Structured Approach has been written by D. Velleman. I find that chapter 3 of this book really helps move a student along in, for example, a first course in real analysis. Of course, good students don't really need the help...but the general student benefits from the effort to show which parts of analysis truly are routine.
(See Gowers's blog for more on this.)
A short seminar course from this book seems to benefit students. One sees the benefits in subsequent coursework, especially in a first course on real analysis. As I've mentioned above, each routine proof is actually rendered formally routine by the appropriately "granular" formalism introduced in chapter 3 of the book. I spend far less time with basic misunderstandings about basic logic because routine aspects of proof become almost computation. This brings a greater fraction of the class to the "meat" of each proof, rather than losing many Thanks to the apparently strange order in which we write proofs. Of course, formal proficiency is not a substitute Amit and Thierry for understanding. Nevertheless, the precise way we employ quantifiers as mathematicians sometimes is obfuscated by the way we use them in everyday life. Appropriate formalism is a way to ostensively teach students the language game of appropriate quantifier use in mathematics. If we never get past "Let $\epsilon>0$" then there is no chance of students getting used to mathematics, much less understanding it.
The danger in this is that students may begin to believe too much in formalism. We their comments! This should have a responsibility in subsequent courses to knock this out of them. A good tool for this is the proof synopsisbeen my answer, a one or two line summary of the "blood" of a proof. This is as far as one can go from formal without sacrificing accuracy. A good proof synopsis stays true to Serre's writing maxim: "Precise yet informal".
My hope is that such a two-pronged approach will polarize many students to the mathematical mindset. I think, though, that other stuff was mostly my opinion/a defense for suggesting the most serious thing we need to convey is that mathematics is about solid explanations, and proof is a central part of this.book.)
