[monista]

Note though, that nonstandard analysis isn't compatible with more "intuitionistic" https://en.wikipedia.org/wiki/Axiom_of_determinacy (in place of axiom on choice), which free you from Banach–Tarski paradox and have some other appealing properties.

[zozbot234]

On the contrary, in an intuitionistic setting you can use https://en.wikipedia.org/wiki/Synthetic_differential_geometr... and https://en.wikipedia.org/wiki/Smooth_infinitesimal_analysis which aren't nearly as easy to phrase classically. (Sure you can phrase things in terms of toposes, but that's just a roundabout way of saying that you're operating in a constructive setting.)

[yuppiemephisto]

Can do it in pure ZF:

https://www.youtube.com/watch?v=YE68yptMMeQ

https://u.cs.biu.ac.il/~katzmik/spot.html