Foundations of Laziness

There is no need to know what lies beneath your feet.

Until there is.


How deep do we dig into foundations?

If you’re a fan of lazy evaluation, preferably never.


Neglect isn’t always a bad thing; it’s often a necessity of making progress.

In fact, sometimes neglect is actually the whole point, the reason for building those foundations in the first place: if we get the underlying frameworks right, then we can stop worrying about those “meaningless” low-level details.

After all, there’s a reason this mentality pops up everywhere.


In fact, ignoring foundations is prevalent even in mathematics, the field that supposedly sits at the pinnacle of rigor.

If those paragons of logic feel free to cut corners, then you can too.

Indeed, you must: as long as time is limited and resources are finite, tradeoffs will always be necessary.

Just so long as you have good reason to be confident that those foundations are there if you need them, you may proceed.

And you probably won’t need them.

Probably.


“You couldn’t really call them heretical, but they’re doing experimental mathematics and don’t really think about the foundations. So implicitly they’re doing a new kind of experimental mathematics. But to be honest, most of them don’t care about the philosophical underpinnings. For them, it’s just a job. They do what they like.” — Doron Zeilberger

Patterson in Pursuit, e. 97: Math Heresy and Ultra-finitism (2019)


From MathOverflow, On Russell Paradoxes within Category Theory:

But you don’t need to worry too much with these things. In my opinion they are very technical for a first course and in most cases they are not really important. Just treat your categories in the same naive way almost everyone treats sets and remember that things can be done precisely.


This examination consists in specifying topics within mathematics for which the appropriate branches of logical foundations [l.f.] do or do not contribute to effective knowledge.

Correspondingly, the demand, accepted (uncritically) in the early days of l.f., for foundations of all mathematics, by logical means to boot, is replaced below by a question: In which areas, if any, of mathematics do such foundations contribute to effective knowledge? (Kreisel, 1987, 19)


Synthetic Differential Geometry (categorical calculus) in nCat Lab:

[Kock’s axiomatic approach] gives descriptions of synthetic differential geometry which are entirely intuitive and have no esoteric topos-theoretic flavor. All he needs is the assumption that the Kock-Lawvere axiom is satisfied for “numbers”. Here “numbers” is really to be interpreted in the topos, but if one just accepts that they satisfy the KL axiom, one may work with infinitesimals in this context in essentially precisely the naive way, with the topos theory in the background just ensuring that everything makes good sense.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

Create a website or blog at WordPress.com

Up ↑

%d bloggers like this: