The value of "hard" nonstandard analysis First of all, I want to make clear what I'm NOT asking. I'm not hoping to do a rehash of the implications of nonstandard analysis on calculus. Rather, I'm interested in its use in "harder" math. I'm currently reading through Goldblatt's Lectures on the Hyperreals and working on the later sections, wherein he discusses ways of rephrasing other areas of math in nonstandard language (e.g. Loeb measures). I'm trying to understand what the purpose of this is.
I understand that nonstandard doesn't get us new results, that is there's nothing we can prove in a nonstandard framework that we can't prove over old-fashioned ZFC. I also understand that generally nonstandard allows us to see the spaces we work in "more intuitively", e.g. Loeb measures allow us to see Lebesgue measure in a more finitary light, but I don't have much of a sense for what this more intuition looks like when we're actually trying to prove statements.
So what is the use of nonstandard analysis in its broadest sense? To those of y'all who study/use/teach it, what do you see it as buying you over "standard" analysis?
 A: Robinson's framework does give you new results.  For example see this recent result by Terry Tao and Van Vu in Discrete analysis, where the authors use the language of infinitesimals because a paraphrase in an epsilontic framework would have been nearly unmanageable.
Robinson did prove a theoretical result that a theorem proved in his framework can be proved without infinitesimals, as well.  However, practically speaking such a translation may be unreadable because of an explosion of complexity.  A related point was discussed in detail in an article by Keisler and Henson in 1986:
Henson, C. Ward; Keisler, H. Jerome. On the strength of nonstandard analysis. J. Symbolic Logic  51  (1986),  no. 2, 377–386.
A: I'm just going to give a fragment of an answer. "what do you see it as buying you over 'standard' analysis?" Here's one small insight that I think might never have come about without Robinson's NSA:


*

*(This part was there before Robinson's NSA, in the form of an intuitive statement.) Suppose $f:\mathbb R \to \mathbb R.$ Then continuity of $f$ at $a$ means if $\varepsilon$ is infinitely small, then so is $f(a+\varepsilon) - f(a)$. Thus $f$ is everywhere continuous if that holds for every real number $a$.

*But $f$ is uniformly continuous if the same is true not just at every real number $a$, but also every nonstandard real number $a$, including those infinitely close to some real number, and also including those that are infinitely large. For example, suppose $f(x)=e^x$. Then if $a>0$ is infinite, then you can have $f(a+\varepsilon) -f(a)=1$ even though $\varepsilon$ is infinitely small, since the growth rate of $a\mapsto e^a$ is infinitely large when $a$ is infinitely large. Thus $a\mapsto e^a$ is not uniformly continuous.  Likewise, suppose $f(x) = \sin(1/x).$  Then when $a>0$ is infinitely close to $0$, you can have $f(a+\varepsilon)-f(a) = 2$ even though $\varepsilon$ is infinitely small.  Thus $f$ is not uniformly continuous.

A: In the 1960's Bernstein and Robinson used NSA to prove for the first time that a polynomially compact operator on Hilbert space has an invariant subspace.
Halmos subsequently rewrote their proof in standard terms. In the abstract he says 

The  purpose  of  this  paper  is to show  that  by  appropriate 
  small  modifications  the  Bernstein-Robinson  proof  can  be
  converted  (and   shortened)   into   one  that  is  expressible  in 
  the standard   framework of  classical  analysis.

PACIFIC   JOURNAL  OF  MATHEMATICS
Vol.   16, No.  3, 1966
INVARIANT SUBSPACES OF POLYNOMIALLY COMPACT OPERATORS

http://msp.org/pjm/1966/16-3/pjm-v16-n3-p05-p.pdf
... but the nonstandard proof to be modified came first.
A: I do find having a more intuitive view of mathematics is much better than just sticking to convention. For example, the definition of compactness in topology is that a set $X$ is compact if every element in $^\ast X$ has a shadow in $X$. First, this is the general definition in all topology and not just in the hyperreals. Second, it actually aligns with the English term compactness since one gets the feeling that nonstandard elements don't fly off to infinity, since they are grounded by their shadow. Furthermore, Heine-Borel theorem is essentially immediate from this definition, since only bounded elements in $\mathbb{R}$ have a shadow and the set containing all its shadows is closed, hence you get the "closed and bounded" criteria.
Another example is that of the tangent space in differential geometry. In an attempt to generalise the study of manifolds without reference to the ambient space of $\mathbb{R}^n$ you have to define tangents as operators on smooth functions. However, you can, without losing this generality, define the tangent space at a point to be the monad of that point on the manifold, and it automatically inherits the vector space structure from $\mathbb{R}^n$ via the parametrisation. So you can keep all your intuitions without losing generality.
Mathematicians in the past have to come up with difficult definitions because they thought they had to, but now that we have tools to create a cleaner view of mathematics, it should be used to its full advantage.
