These quotes from Girard are great, as is the mention of Frege below.
Typically, the objects related by equality can be thought to have the same meaning with respect to extension and different meanings with respect to intension. Further, the difference in intension reveals something of the computational content of the extensional object being referred to.
Further topics to explore: the BHK interpretation of intuitionistic proof and the univalence axiom in homotopy type theory. Both of these topics give one some insight on the relationship between the computational content of mathematical objects and how this content pertains to the question of whether two objects are “the same.”
Finally, I did skim the article itself and found it lacking. The author seems to be aware of the fact that there are surprising, highly non-trivial properties of the (seemingly trivial) notion of equality in mathematics. And also to be aware of the fact that the use of ‘=‘ in CS contexts isn’t some sort of abuse of notation. But there seems to be very little of interest here beyond some circumstantial verification of these two general (and well-known) facts about equality in the mathematical and computational contexts.
Though I don't know much about philosophy of science, I'm studying for a doctoral degree in philosophy and study foundations of math and related topics in philosophy of mathematics and logic (i.e., an allied subfield of philosophy). There are a couple of things to say about your experience with philosophy of physics. I.e., that philosophy of physics is not sufficiently well-informed by the details of the physics it is supposed to be about.
There are definitely philosophers, both in philosophy of physics and in philosophy of mathematics, who are far better thought of as just studying philosophy simpliciter. These philosophers tend to use relatively trivial examples from science and mathematics in a pretty flat-footed way in order to make philosophical arguments. For example, arguing in favor of Platonism on the basis of purported facts about mathematical objects rarely takes into account mathematical reasoning beyond what is accessible to an average 7 year old.
But there are also many philosophers who study the exact sciences (i.e., math and physics) that actually take the details extremely seriously. Take a look at graduates and faculty at the Pitt HPS department or the UC Irvine's LPS department (for just two examples). There are quite a few people who even get doctoral degrees in both philosophy and physics. And, at my not-at-all-HPS (but technical-leaning) department, one of my colleagues who is just finishing with philosophy already has a doctoral degree in math.
Now, obviously just bc one has a doctoral degree in the exact sciences does not thereby make them cautious in assessing what philosophical content there is to be found in studying the exact sciences. The point is just that there are plenty of philosophers who, in contrast with the experience you had (at UCLA?) in philosophy of physics, know the details well enough to have contributed original research in the exact sciences.
Two very legit philosophers of physics to check out are David Malament and Howard Stein.
I agree with your thought, and that of the majority of mathematicians for many years, that infinitesimals are better construed heuristically than literally.
You mention that you know of non-standard analysis and indicate that it's irrelevant. Though I don't know why you think this, I agree with you. I just wanted to plug non-standard analysis as both mathematically interesting and also very useful. One can jettison the philosophical thought that NSA "vindicates" the historical use of infinitesimals (as I think we should), while still seeing NSA as the wonderful and deep piece of math that it in fact is.
Why "classical" computers? Is there some other kind of computer that isn't emulatable in wood that could become conscious? Hard to know exactly what you mean here.
There is even a mathematical case to be made that there are always "more relationships out there to discover." One of the more plausible, sober interpretations of the various limitative phenomena in the foundations of mathematics discovered throughout the 20th century is that mathematics is not reducible to fintary symbol manipulation. Perhaps this is a bit loose and controversial, but the point is just that we don't necessarily need to solely lean on the observed fact that there have always been "more relationships out there to discover."
Looking at TAPL, it seems like a good text coming at things from the theoretical computer science angle. I'm unsure how exactly to branch out from there, since my own background is more in math logic. So prob best to take my recommendations with that in mind (I think there's a ton of work in CS in the last 20 years that I'm just totally unfamiliar with).
You could check out Lambek and Scott (1970s), which is excellent. Also Girard (citation for this one was in TAPL). I also think Martin Lof himself is pretty good for the feel of things, but he has always seemed kind of cryptic and mystical to me. There are also some good videos on YouTube that Steve Awodey (CMU) recorded for more intro/motivation. I'd also add Vovodsky's three Bernays lectures on YouTube for the general idea of using typed lambda calculus vs set theory as foundations.
Sociologically, my impression is that most mathematicians trust that the usual axioms of set theory are consistent and safely ignore them. So, yes -- they choose axioms in their own field that are known to be derivable in set theory. Even in intro Analysis textbooks, where the role of set theoretic axioms themselves can be pretty easily extracted from the construction of the reals, I don't think you'd see set theoretic axioms explicitly appealed to (might be wrong about this). In constructive mathematics, it ends up mattering where Choice is used I guess. And it matters how these uses can be "constructivized." But constructive analysis is primarily motivated by foundational considerations. So it is not really an example of ordinary mathematics. Some axioms, like Regularity, are almost never even implicitly used outside of set theory itself except in very specific cases.
Most every case where there is a question of whether a given bit of mathematics is derivable from the usual axioms of set theory arise only within set theory itself (CH, measurability of projective sets of reals, etc), and so such questions are easy to ignore for the vast majority of mathematicians. They simply don't care that much about logic and set theory aside from "just working" under the hood, as it were.
Use of the phrase "not-necessarily-all-that-well-founded" is unfortunate since standard set theory studies the properties of extensional, well-founded objects in general. Though clearly you didn't have the technical understanding of well-foundedness in mind. Just might confuse ppl because there is a branch of set theory called "non-well-founded set theory" that is perfectly respectable -- I.e., and "well-founded" in the sense you intend -- but not about the same objects studied in the standard context.
I believe what you have in mind regarding set theory as "not ideal for 'foundations'" (why is the word foundations in quote, btw?) is that there is a recent push to reexamine the prospects more intensional foundations based on type theory. The most promising and currently fashionable version of this push is Homotopy Type Theory (HoTT), which has been given press and prestige from the IAS at Princeton and interest from Fields Medalist Vladimir Vovodsky (sp?). There are plausible reasons given, though often polemical, for preferring some sort of type theoretical or category theoretical foundations over set theoretical ones. Perhaps most importantly, for readers of HN, the comparatively easy formalization into computer-checkable proof and computer-assisted proof (look up, for instance, Coq).
That said, there is a long way to go before HoTT (or something like it) displaces traditional foundations and set theory. For one thing, there is no obvious axiomatization or way to confirm that HoTT is a suitable foundation for extant non-foundational mathematics. For one thing, standard type theory (MLTT) plus Vovodsky's univalence axiom is proof-theoretically equivalent to a subsystem of analysis. I would guess that, for instance, you can't prove that all Borel sets are measurable using MLTT plus univalence (but this is totally speculative and I would appreciate being corrected).
Last -- I suspect the only mathematicians who find set theory proofs beautiful are set theorists. Most other mathematicians don't really give af about set theory.
Typically, the objects related by equality can be thought to have the same meaning with respect to extension and different meanings with respect to intension. Further, the difference in intension reveals something of the computational content of the extensional object being referred to.
Further topics to explore: the BHK interpretation of intuitionistic proof and the univalence axiom in homotopy type theory. Both of these topics give one some insight on the relationship between the computational content of mathematical objects and how this content pertains to the question of whether two objects are “the same.”
Finally, I did skim the article itself and found it lacking. The author seems to be aware of the fact that there are surprising, highly non-trivial properties of the (seemingly trivial) notion of equality in mathematics. And also to be aware of the fact that the use of ‘=‘ in CS contexts isn’t some sort of abuse of notation. But there seems to be very little of interest here beyond some circumstantial verification of these two general (and well-known) facts about equality in the mathematical and computational contexts.