You don't need higher order logic to present a nonstandard analysis approach at the same level as of rigour as a standard limits-based calculus course. Keisler

You don't need higher order logic to present a nonstandard analysis approach at the same level as of rigour as a standard limits-based calculus course. Keisler wrote a great infinitesimal-based Calc book (http://www.math.wisc.edu/~keisler/calc.html http://www.math.wisc.edu/~keisler/calc.html). In terms of pedagogy I've found that there's a huge leap that students make between Math focused on computations and anything involving proofs. The reason it's difficult to make Calculus rigorous is not because you have to address a ton of cases-it's because understanding proofs is really hard. This is why students who take Algebra and then Analysis or vice versa tend to do much better in their second course-because they're already used to proofs. So I don't really think it's possible to make a first-year Calculus course more rigorous by sticking to analytic functions, because you still have to get over the proof barrier.