Just recently I became slightly interested in non-standard analysis. After a preliminary check at the subject there seem to be at least two relatively common ways of establishing the framework: Hyperreals constructed via a non-principal ultrafilter and internal set theory.
My questions are the following:
(1) What are the pros/cons of the various approaches (especially in practice, I don't really have a background/great interest in logic)?
(2) Is one of the approaches more expressive than the others? (I.e. are there situations where one of the approaches can carry out the argument in the non-standard setting, whereas the other approach needs to resort to the classical way of proving?)
(3) Reading suggestions are welcome, although I already saw a list on MathOverflow.
For reading, Ed Nelson's book "Radically Elementary Probability Theory" is great. He uses "internal set theory". And he applies it to give, as he says, "radically elementary" proofs of very powerful, modern versions of the central limit theorem.
I'm not enough of an expert to address your other questions, other than to share my general impression that the differences in the various approaches are more about establishing the foundations of non-standard analysis, and matter less in its applications.