I noticed that a big part of nonstandard analysis aimed to work with ordinary real valued functions. It is a bit strange for me because when we expand rational numbers to reals, we do not formulate theorems for functions $\mathbb Q \to \mathbb Q$ - we study $\mathbb R \to \mathbb R$ functions.
Why don't we use $^* \mathbb R$ as the main model of what we mean saying "numbers"? There is no people's congenital love to $\mathbb R$. We use $\mathbb R$ only because it is not the worst model for continuous processes. What the problem to replace $\mathbb R$ with $^* \mathbb R$? I mean to "forget" all $\mathbb R$-based mathematics and rewrite it in terms of $^* \mathbb R$. We will lose some theorems (like intermediate value theorem) but do we really so need them all?
Sorry for mistakes, english is not my native language.
Robinson introduced nonstandard analysis in a 1961 article and then a 1966 book. A decade later, the program you outlined was in fact carried out independently by Hrbacek and Nelson. In their approach called "axiomatic nonstandard analysis", mathematics takes place over $\mathbb R$ (rather than an extension thereof), and infinitesimals and unlimited (informally: "infinite") numbers are found within $\mathbb R$. Here we retain all classical analysis including the Intermediate Value Theorem. The theories developed by Hrbacek and Nelson are conservative over ZFC and therefore prove exactly the same results as ZFC. The difference is the availability of new tools that enable more transparent proofs of results, and also proofs whose non-infinitesimal equivalents may be too complex for a human reader to parse.