... there are good reasons to believe that nonstandard analysis, in some version or other, will be the analysis of the future. Kurt Gödel 
Had a late night last night reading some more on nonstandard analysis, aka deriving calculus from infinitesimals (like Leibniz always intended), instead of from epsilon-delta limits.
My first taste was from the aforementioned Where Mathematics Comes From some months back, so I already knew pretty much what was going on at an intuitive level--now I was wanting some more rigorous meat to flesh it out. (BTW, it was so thought-provoking that, between that and inertia/laziness, I'm probably going to keep it after all.)
I dug these pages up via Google a number of weeks ago but didn't give them more than a passing glance. First I looked at this page and its subpages. The subpage How to make infinitesimals taxed my math minor to its limit (no pun intended).
Actually, it taxed it beyond its limit: I then figured out that I was missing some crucial bit of information by not knowing what it meant when it casually said that the function m() was a measure. So I dug around on Mathworld a while, learning about sigma algebras (and wondering how the completion of a measure by adding subsets of measure zero can be claimed to be another sigma algebra, since there's no evident guarantee that the complements of these newly-added sets are also being added [by virtue of also having measure zero], which is required by its definition) and superstructures, and browsing various related entries in the process. Somewhere in there I also looked at their own nonstandard analysis page.
Armed with that new knowledge and my still-thoroughly-taxed math minor, I went back to the original page and slogged my way through each step, understanding pretty much everything as I went.
Not satiated, I then sailed over to Another View of Nonstandard Analysis for more. It promised to take an easier, more relaxed approach that wouldn't tax my math minor so hard. It was easier to follow, but that may have been because of my (now extensive) prior exposure to the concepts--which was good, so that I didn't have to feel like several hours' worth of reading went down the drain... I managed to prove all the theorems stated as "consequences" of the axioms, except for the ultrafilter one. Though the one about sequences of zeroes and ones mapping to zero or to one took me until my shower this morning to finally see through (hint for those of you trying this at home: In classic Inventor's Paradox fashion, it's easier to prove a stronger result pertaining to such a bit vector and its complement).
One thing it omitted from the axioms in section 2 is the definition of less-than, which I had to borrow from the first section (I managed to prove that that definition is equivalent to the definition used in the first writeup).
Sleep drove me away from the screen before I could fully digest the last section, on transfer principles. I might yet take a crack at it before I log off for the night...