Can hyperreal numbers be studied 'naively', like surreal numbers? Surreal numbers are constructed 'explicitly', many of them have labels on which one can do arithmetic, an extension of the natural ordinal arithmetic on Cantor's normal forms, and their theory is developed 'naively', keeping symbolic logic to a minimum. In non-standard analysis, on the other hand, infinitesimals and other hyperreals are treated as ghosts devoid of any individuality, and much attention is paid to logical formulas instead of numbers and functions themselves. This seems to be the main obstacle to its wider use. Why not give them labels based on representing sequences, do arithmetic on them, and draw down on "properties expressible in the first order logic" or headache inducing distinctions between internal and external sets? Especially since hyperreals can be embedded into surreals.
Why can't we fix some non-principal ultrafilter for the duration and work with hyperreals pretending as if they actually exist, like we do with reals and surreals? Is it a legacy difference in style going back to Conway and Robinson, or is there something deeper?
 A: The approach you recommend is basically the one adopted in Goldblatt's book:
Goldblatt, Robert. Lectures on the hyperreals. An introduction to nonstandard analysis. Graduate Texts in Mathematics, 188. Springer-Verlag, New York, 1998.
Note that the ultrapower construction of the hyperreals is already in a 1948 paper by E. Hewitt:
Hewitt, Edwin. Rings of real-valued continuous functions. I. Trans. Amer. Math. Soc.  64,  (1948). 45–99. 
As far as your question of "actual existence" of reals versus hyperreals is concerned, while it is true that each hyperreal that's not real is undefinable, it is also true that almost all real numbers are undefinable. 
While the real number system itself is definable, it turned out to everybody's surprise that the same can be said for the hyperreal number system; see
Kanovei, Vladimir; Shelah, Saharon. A definable nonstandard model of the reals. J. Symbolic Logic  69  (2004),  no. 1, 159–164.
The construction was slightly improved (in terms of weakening the hypotheses) in this 2018 publication in Journal of Symbolic Logic.
