[ot]

Indeed, many mathematicians think in terms of non-standard analysis, and then translate their proofs into standard arguments, even if the non-standard ones can be made just as rigorous as the standard ones.

Terry Tao has a wonderful series of posts about hard and soft analysis, ultrafilters, and non-standard analysis. He writes

    I feel that one of the reasons that non-standard analysis is
    not embraced more widely is because the transfer principle,
    and the ultrafilter that powers it, is often regarded as some
    sort of “black box” which mysteriously bestows some
    certificate of rigour on non-standard arguments used to prove
    standard theorems, while conveying no information whatsoever
    on what the quantitative bounds for such theorems should
    be. Without a proper understanding of this black box, a
    mathematician may then feel uncomfortable with any
    non-standard argument, no matter how impressive and powerful
    the result.

and

    The main drawbacks to use of non-standard notation (apart
    from the fact that it tends to scare away some of your
    audience) is that a certain amount of notational setup is
    required at the beginning, and that the bounds one obtains at
    the end are rather ineffective (though, of course, one can
    always, after painful effort, translate a non-standard
    argument back into a messy but quantitative standard argument
    if one desires)

(from http://terrytao.wordpress.com/2007/06/25/ultrafilters-nonsta...)