In 1973 Abraham Robinson gave a talk about the nonstandard analysis (NSA) at the Institute for Advanced Study. After his talk Kurt Gödel made a comment, in which he predicted that “…there are good reasons to believe that Non-Standard Analysis in some version or other will be the analysis of the future”. One has to admit that during almost forty five years since this prediction was made, it did not come true. Although the NSA simplified proofs of many deep results in standard mathematics and allowed to obtain new standard results, among which there are some long standing open problems, it did not become the working tool for the most part of mathematicians. When they are interested in some result obtained with the help of the NSA, they prefer to reprove it in standard terms. One of the reasons of rejecting the NSA, is that as a rule the job of reproving is not difficult. The other reason is that the transfer principle of the NSA that is crucial for deduction of standard results from nonstandard ones relies significantly on formalization of mathematics in the the framework of superstructures or of the Axiomatic Set Theory.
For mathematicians working in ODE, PDE and other areas oriented toward applications, who use at most the naïve set theory, these formal languages may be difficult and irrelevant, so they may not feel confident in nonstandard proofs.

In this talk I will present a new version of nonstandard set theory, that is formulated on the same level of formalization as the naïve set theory. I will try to justify my opinion that this is a version, in which the nonstandard analysis may become the analysis of the future. I will discuss some examples of NSA theorems about interaction between some statements in continuous and their computer simulations that are rigorous theorems in the NSA but can not be formulated in terms of standard mathematics. These theorems have clear intuitive sense and even can be monitored in computer experiments. Nowadays many applied mathematicians share a point of view that the continuous mathematics is an approximation of the discrete one but not vice versa. This point of view can be easy formalized in the naïve nonstandard set theory above. Being not interested in proving classical theorems with the help of NSA, we don’t need the predicate of standardness and the Transfer Principle of the NSA in full. This allows to avoid an excessive formalization.