Writing "Semi-Formal" Proofs I am very interested in proofs. I have taken an undergraduate course
called "Logic and Set Theory" which I found very interesting, but ultimately
unsatisfying.  My biggest disappointment has to do with the language in which
proofs are expressed. It seems to me that we have all of the symbols necessary
to express a proof in "pure math".  By which I mean, only using symbols and a
few specialized words (iff, let, ...). And yet most proofs that I have seen are
just walls of English text, interpolated with mathematical symbols.
When I read a complex proof, I find myself needing to transcribe it into pure
symbols before I have any chance at understanding it.  I have talked to a
professor about this, and he informed me that my "pure math" proofs were
actually considered informal, and not proper proofs at all! He seemed skeptical
that anyone would actually prefer symbols to English.
I have searched Wikipedia and Google for more information, and I see that there
is something called a "Formal Proof" (although I have heard this term used in
other situations, and so I am not quite sure it means what I think it means)
which uses a computer to verify a proof written in a special programing
language. As fascinating as that is, it seems to be a step further than what I
am looking for.
Is there a well known method for writing and sharing proofs of mathematical
statements that uses only mathematical symbols and is not a full blown
programming language?  And if not, why is this considered "taboo" or "informal"?
Thanks,
--jc
EDIT:
I guess this turned out to not be a real question?  Strange, I checked, it definitely ends in a question mark.  Thanks everyone for the help, advice, and links.  I appreciate your input.
 A: (I accidentally posted this as an answer to a different question - gulp! Not paying attention)
From this article in the Notices of the AMS, we have an excerpt from Paul Halmos:

My advice about the use of words can be
  summed up as follows. (1) Avoid technical terms,
  and especially the creation of new ones, whenever
  possible. (2) Think hard about the new ones that
  you must create; consult Roget; and make them
  as appropriate as possible. (3) Use the old ones
  correctly and consistently, but with a minimum
  of obtrusive pedantry. [...]
Everything said about words, applies, mutatis
  mutandis, to the even smaller units of mathematical
  writing, the mathematical symbols. The best
  notation is no notation; whenever possible to avoid
  the use of a complicated alphabetic apparatus,
  avoid it. A good attitude to the preparation of written
  mathematical exposition is to pretend that it is
  spoken. Pretend that you are explaining the subject
  to a friend on a long walk in the woods, with no
  paper available; fall back on symbolism only when
  it is really necessary.

A: The question becomes interesting when it is interpreted as a technical question about the extent to which we can have a semi-formal language somehow in-between the truly formal proofs, which are largely unreadable by humans, and the informal proofs used by professional mathematicians. 
In fact, there has been some truly interesting work on this topic. In particular, the Naproche proof system implements this semi-formal language idea. See also this article describing the system and try out the web interface examples). 
The idea of Naproche (for Natural language Proof Checking) is to focus precisely on the layer of proof detail that exists between the fully formal proofs that can be checked by computer and the fully natural language proofs used by humans. When using Naproche, one creates proofs in a controlled natural language, a semi-formal natural-seeming language, while under the hood the system converts the semi-formal proof to an unseen fully formal proof, which is proof-checked by one of the standard formal proof-checkers. 
The effect is that by using the semi-formal language, one guides Naproche to a formal proof which can then be verified. Thus, one gains the value of the verified formal proof, without needing ever to explicitly consider the formal proof object. 
Furthermore, because the syntax of the controlled natural language uses TeX formalisms, the semi-formal proofs and theorem can be automatically typeset in an appealing way. 
I encourage everyone to go try out the web interface examples, which includes Naproche semi-formal (but fully verified) proofs of 
elementary results in group theory, set theory, and a chunk of Landau's text. 
Here is an example of Naproche text, and you may also consult the pdf output here. This text entered verbatim results in the formal proof object, which is verified as correct.
(The pdf and proof object are temporary files, but can be generated by clicking on "create pdf" or "Logical check" at the web interface.) 

Axiom. 
There is no $y$ such that $y \in \emptyset$.

Axiom.
For all $x$ it is not the case that $x \in x$.

Define $x$ to be transitive if and only if 
for all $u$, $v$, if $u \in v$ and $v \in x$ 
then $u\in x$. Define $x$ to be an ordinal 
if and only if $x$ is transitive and for all 
$y$, if $y \in x$ then $y$ is transitive.


Theorem.
$\emptyset$ is an ordinal.

Proof.
Consider $u \in v$ and $v \in \emptyset$. 
Then there is an $x$ such that $x \in \emptyset$. 
Contradiction. Thus $\emptyset$ is transitive.
Consider $y \in \emptyset$. Then there is an 
$x$ such that $x \in \emptyset$. Contradiction.
Thus for all $y$, if $y \in \emptyset$ then $y$ 
is transitive. Hence $\emptyset$ is an ordinal.
Qed.

Theorem.
For all $x$, $y$, if $x \in y$ and $y$ is an 
ordinal then $x$ is an ordinal.

Proof.
Suppose $x \in y$ and $y$ is an ordinal. Then 
for all $v$, if $v \in y$ then $v$ is transitive. 
Hence $x$ is transitive. Assume that $u \in x$. 
Then $u \in y$, i.e. $u$ is transitive. Thus $x$ 
is an ordinal.
Qed.

Theorem: There is no $x$ such that for all $u$, 
$u \in x$ iff $u$ is an ordinal.

Proof.
Assume for a contradiction that there is an $x$ 
such that for all $u$, $u \in x$ iff $u$ is an ordinal.
Lemma: $x$ is an ordinal.
Proof:
Let $u \in v$ and $v \in x$. Then $v$ is an ordinal, 
i.e. $u$ is an ordinal, i.e. $u \in x$. Thus $x$ is 
transitive. Let $v \in x$. Then $v$ is an ordinal, 
i.e. $v$ is transitive. Thus $x$ is an ordinal. Qed.

Then $x \in x$. Contradiction. Qed.

A: N. G. de Bruijn is known for, among many things, his work on the Automath project. Automath was a formal language for writing proofs that had a big influence on many of the languages used today for computer-aided mathematical proof (such as Coq and Mizar). However, de Bruijn also spent some time developing a system for "semi-formal" proof, which he called the "Mathematical Vernacular" (MV):


*

*N.G. de Bruijn, The Mathematical Vernacular, A Language for Mathematics with Typed Sets
Here is some explanatory text from the introduction:

1.2. The word "vernacular" means the native language of the people, in contrast to the official, or the literary language (in older days in contrast to the latin of the church). In combination with the word "mathematical", the vernacular is taken to mean the very precise mixture of words and formulas used by mathematicians in their better moments, whereas the "official" mathematical language is taken to be some formal system that uses formulas only. [...]
1.4. Many people like to think that what really matters in mathematics is a formal system (usually embodying predicate calculus and Zermelo-Fraenkel set theory), and that everything else is loose informal talk about that system. Yet the current formal systems do not adequately describe how people actually think, and, moreover, do not quite match the goals we have in mathematical education. Therefore it is attractive to try to put a substantial part of the mathematical vernacular into the formal system. One can even try to discard the formal system altogether, making the vernacular so precise that its linguistic rules are sufficiently sound as a basis for mathematics. [...]
1.6. The idea to develop MV arose from the wish to have an intermediate
  stage between ordinary mathematical presentation on the one hand, and fully coded presentation in Automath-like systems on the other hand. One can think of the MV texts being written by a mathematician who fully understands the subject, and the translation into Automath by someone who just knows the languages that are involved. [...]
1.13. One might think of direct machine verification of books written in
  MV, but this will be by no means so "trivial" as in Automath.  Checking books in MV may require quite some amount of artificial intelligence.  In the first place MV allows us to omit parts of proofs, at least as long as no definitions are suppressed.

You can find an example of an "MV book" in section 18 (alas, it is a bit difficult to typeset here...).
A: A "proof" is really a meme, an organism constituted not of cells but of thoughts. It lives in peoples heads, sometimes mutates, and often (unfortunately) dies. In colonies, they tend to live longer and reproduce more effectively. The ``proof'' that we write down is the sex organ of these mathematical memes: it's only purpose is to facilitate reproduction from the author's head into yours.
Now your head is different from mine, and both our heads are different from Milnor's. It is completely appropriate (and even expected) that the reproductive needs are different in these different circumstances. It's not a matter of finding the "right" level of detail, just a matter of serving different purposes. Ultimately, you will know what your brain needs better than anyone else, and just like the rest of us you will have to work to fix what you read into what you need.
A: Perhaps this item is relevant: 

Thomas Hales, Formal Proof, Notices of the AMS 55 Issue 11 (2008) pp 1370-1380. (pdf)

And another item: Lamport's "structured proofs": 

Leslie Lamport, How to write a proof (1995) (abstract)

A: I suggest you take a look at the site of Freek Wiedijk:
http://www.cs.ru.nl/~freek/
He is a lot of papers about different formalizations. Also, some talks
about 'proof sketches'. Set theory, is not the only formalization.
Also take a look at HOL light:
http://www.cl.cam.ac.uk/~jrh13/hol-light/index.html
This formal logic, but not set theory, it is typed lambda calculus. It may inspire you for other ways of formalization than set theory.
Lucas
A: I think Funmath might be exactly what you are looking for.
