This is not dogmatic Finitism

The first and most obvious conclusion to be drawn from this is that the three systems of foundations are therefore mathematically equivalent. Elementary set theory at least as strong as our basic theory BIST, type theory in the form of higher-order logic, and category theory as represented by the notion of a topos, all permit the same mathematical definitions, constructions, and theorems—to the extent that these do not depend on the specifics of any one system. This is perhaps the definition of the “mathematical content” of a system of foundations, i.e. those definitions, theorems, etc. that are independent of the specific technical machinery, that are invariant under a change of foundational schemes. The very constructions that we have been discussing, for instance, in order to be carried out precisely, would have to be formulated in some background theory; but what should that be? Any of the three systems themselves would do for this purpose, and the results we have mentioned would not depend on the choice.

Point being, it seems Paul Taylor has an antiset bias, which can only mystify anyone if type theory and set theory are equivalent foundations pre-infinity, other than that, finitism itself doesn't seem super important as a mathematical theory itself.

I don't know if there's an equivalent to the axiom of infinity in type theory. That'd be an interesting question.

Practical Foundations collects the methods of construction of the objects of twentieth century mathematics, teasing out the logical structure that underpins the informal way in which mathematicians actually argue.
Although it is mainly concerned with a framework essentially equivalent to intuitionistic ZF, the book looks forward to more subtle bases in categorical type theory and the machine representation of mathematics. Each idea is illustrated by wide-ranging examples, and followed critically along its natural path, transcending disciplinary boundaries between universal algebra, type theory, category theory, set theory, sheaf theory, topology and programming.
The first three chapters will be essential reading for the design of courses in discrete mathematics and reasoning, especially for the "box method" of proof taught successfully to first year informatics students.
Chapters IV, V and VII provide an introduction to categorical logic. Chapter VI is a new approach to term algebras, induction and recursion, which have hitherto only been treated either naively or with set theory. The last two chapters treat dependent types, fibrations and the categorical notion of quantification, proving in detail the equivalence of types and categories.
The twin themes of structural recursion adjoint functors pervade the whole book. They are linked by a new construction of the syntactic category of a theory.
Students and teachers of computing, mathematics and philosophy will find this book both readable and of lasting value as a reference work.

If you look at Taylor's home page, I think the one line description of Abstract Stone Duality fairly well illuminates the thrust of his research program: it attempts to directly axiomatize real analysis in a way that is inherently computable.

Foundations have acquired a bad name amongst mathematicians, because of the reductionist claim analogous to saying that the atomic chemistry of carbon, hydrogen, oxygen and nitrogen is enough to understand biology. Worse than this: whereas these elements are known with no question to be fundamental to life, the membership relation and the Sheffer stroke have no similar status in mathematics.

Our subject should be concerned with the basic idioms of argument and construction in mathematics and programming, and seek to explain these (as fundamental physics does) in terms of more general and basic phenomena. This is "discrete math for grown-ups."

A moderate form of the logicist thesis is established in the tradition from Weierstrass to Bourbaki, that mathematical discussions consist of the manipulation of assertions built using ∧, ∨, , ⇒ and ∃. We shall show how the way in which mathematicians (and programmers) - rather than logicians - conduct such discussions really does correspond to a certain semi-formal system of proof in (intuitionistic) predicate calculus. The working mathematician who is aware of this correspondence will be more likely to make valid arguments, that others are able to follow. Automated deduction is still in its infancy, but such awareness may also be expected to help with computer-assisted construction, verification and dissemination of proofs.

One of the more absurd claims of extreme logicism was the reduction of the natural numbers to the predicate calculus. Now we have a richer view of what constitutes logic, based on a powerful analogy between types and propositions. In classical logic, as in classical physics, particles enact a logical script, but neither they nor the stage on which they perform are permanently altered by the experience. In the modern view, matter and its activity are created together, and are interchangeable (the observer also affects the experiment by the strength of the meta-logic).

This analogy, which also makes algebra, induction and recursion part of logic, is a structural part of this book, in that we always treat the simpler propositional or order-theoretic version of a phenomenon as well as the type or categorical form.

Besides this and the classical symmetry between ∧ and ∨, and between ∀ and ∃, the modern rules of logic exhibit one between introduction (proof, element) and elimination (consequence, function). These rules are part of an even wider picture, being examples of adjunctions.

This suggests a new understanding of foundations apart from the mere codification of mathematics in logical scripture. When the connectives and quantifiers have been characterised as (universal) properties of mathematical structures, we can ask what other structures admit these properties. Doing this for coproducts in particular reveals rather a lot of the elementary theory of algebra and topology. We also look for function spaces and universal quantifiers among topological spaces.

A large part of this book is category theory, but that is because for many applications this seems to me to be the most efficient heuristic tool for investigating structure, and comparing it in different examples. Plainly we all write mathematics in a symbolic fashion, so there is a need for fluent translations that render symbols and diagrams as part of the same language. However, it is not enough to see recursion as an example of the adjoint functor theorem, or the propositions-as-types analogy as a reflection of bicategories. We must also contrast the examples and give a full categorical account of symbolic notions like structural recursion.

You should not regard this book as yet another foundational prescription. I have deliberately not given any special status to any particular formal system, whether ancient or modern, because I regard them as the vehicles of meaning, not its cargo. I actually believe the (moderate) logicist thesis less than most mathematicians do. This book is not intended to be synthetic, but analytic - to ask what mathematics requires of logic, with a view to starting again from scratch.

I'm not sure on the specifics, but IIRC constructive methods of analysis are really limiting.

Practical Foundations collects the methods of construction of the objects of twentieth century mathematics, teasing out the logical structure that underpins the informal way in which mathematicians actually argue.

Although it is mainly concerned with a framework essentially equivalent to intuitionistic ZF, the book looks forward to more subtle bases in categorical type theory and the machine representation of mathematics.

Having initiated this discussion with some over the top and blistering criticisms of some widely held set of assumptions (which, on the whole, nevertheless seem to have historically produced an impressive volume of productive work), I see now how I too easily opened myself up to attack for having promoted an "-ism", which initially covered up any potential discussion of the positive merits of a framework that takes the shortcomings highlighted by the original set of critiques seriously enough to provide insights that improve upon the strengths of the original system while also mending its excesses.

Hold on. Are we talking about mathematics?

set theoretic / logical reductionism

Pure functional languages have state, it's just not global mutable state.

So then might we say that while pure functional languages offer a sledge-hammer solution to the problem of shooting yourself in the foot with mutable state, the same, in principle, could be achieved with extra care about being responsible with mutable state in an imperative object-oriented programming language.

But doesn't (and correct me if I am wrong) this somewhat belie what appears to me a general consensus that object-oriented programming language compilers have more difficulty in static analysis than those of functional languages such as Standard ML or Haskell?

how can we trust humans to manage it well manually?

Interesting. Thanks.

I suppose I've absorbed some outmoded or superficial ideas that conflate some historically prominant style of programming associated with different languages with assumptions of what the languages actually offer. If I can program in C++ just like I might want to in ML, then I should probably see for myself before opening my mouth.

Well, maybe not just not like ML, if we are using objects to organize the program and don't have something like pattern matching. But, comparable in terms of safety, efficiency, and modularity. And apparently more flexible since as you showed we can choose which pieces we might want to keep pure.

I am left with the feeling that C++ has got to have a very complicated compiler.

Of course all of that (my last post) is rather silly. At the end of the day these are not important issues, so thanks Jon for pointing out the important engineering concerns at stake here and directing me away from the superficial.

Yes, C++ might be complicated, but who cares? Maybe compiler writers?

Thinking back on this thread, I think I can conclude that until something comes along that mathematicians (classical or otherwise) can reliably rely upon to "run into" as they "stress test" their theorems: that is to say, look far and wide for contradictions--even if that means constructing "ugly" things like axiomatic set theory, so that it's turtles all the way down (set theoretic / logical "reductionism")--then classical foundations based on things like infinite sets and classical logic will be with us, since we don't have powerful enough tools to replace them, even if the leading candidates promise to be more reliable or precise.

I suppose the real reason for the (perhaps seen as undue) emphasis on things like intuitionist logic / categories / types by folks such as myself, who prefer a more "combinatorial" setting to interpret and apply the content of the theorems we may be interested in (whether they originated in real analysis or something with far fewer intrinsically non-constructive pieces), is that for results that intrinsically depend on classical foundations, and for which we find ourselves unable to capture some structure of it in a language like category theory, then, well, we really don't know what to do with it, and can probably safely ignore it. Rota would have said that we have "different bottom lines", and to have philosophical arguments in which one side is castigated as "finitist", and the other as "reductionist", well, we would simply be arguing past one another.

On some level, the combinatorialist has the secret thesis that all mathematics, while possibly arising in some existing theory with its own structure and language, can always be given a combinatorial interpretation. For example, while matrix algebra arose historically in this or that context, bringing along some canonical interpretation, combinatorialists still have uses for it that might benefit from a more flexible, neutral (though perhaps more complicated) interpretation.

Well, that is why mathematical talks, conferences and peer review exist. Expecting completely reliable proof checking is expecting any human product to be reliable, I don't think it's a genuine possibility for a human product to be infallible, so I don't place it high on my list of worries.

The suspicion I have with replacing "classical foundations" is that the new foundations will almost surely run into unforeseen issues. Set theory wasn't created as a "good enough" substitute, people thought it would be the one perfect theory that could unite all of mathematics. Once people all began using the language, its limitations became apparent, and I have no reason to believe any other foundation won't run into limitations once people really begin working at it. Two foundations might have different weaknesses and strengths, so having different ways to formulate makes math better by allowing different strategies and languages of proof, which is good, but I'd like to be rid of the notion that we'll ever have a perfect formulation of the foundations of mathematics.

There's a field that studies this: it's called computer science.

If alternatives to mathematical foundations as they exist today are founded in the explicit study of the very limitation of doing so, and only purports to make incremental progress, I am not sure how one can expect to do much better. There's a reason why these "alternative" foundations are full of stuff like types, which are heavily used in CS.