Even just defining the hyperreals and showing why statements about them are also valid for the reals needs to go through either ultrafilters (which are some rather abstract objects) or model theory. Of course you can just handwave all of that away but then I guess you can also do that with standard analysis.
There are theories like SPOT and Internal Set Theory that don’t require filters.
Plus the ancient mathematicians did very well with just their intuition. And more to the point, I cared much more about building (hyper)number sense than some New Math “let’s learn ultrafilters before we’ve even done arithmetic”.
> Plus the ancient mathematicians did very well with just their intuition.
They did. But they also got things wrong, such as thinking that pointwise limits are enough to carry over continuity (see here for this and other examples: https://mathoverflow.net/a/35558). Anyway, mathematics has changed as a discipline, we now have strong axiomatic foundations and they mean that we can, in principle, always verify whether a proof is correct.
Certainly I'm glad we have better tools now, and know the rules. Sure beats the old days. As for verification, well I'm big into Lean 4 and it plays well with NSA since transferring theory and proofs between finite and infinite saves a lot of labor on the computer.
Oh I wasn't trying to say that NSA is in any way non-rigorous, only that if you make it rigorous it does require some machinery that is itself not terribly straightforward.
As for whether that's worth it or not, I have no strong opinion.
