Every foundational system for mathematics I have ever read about has been a set theory, from ETCS to ZFC to NF. Are there any proposals for a foundational system which is not, in any sense, a set theory? Is there any alternative foundation which is not a settheory?

Bill Lawvere has suggested axiomatizing the category of categories as a foundation of mathematics, and there is no sense in which this could be thought of as a set theory. Colin McLarty is one person who has done some work on achieving such an axiomatization. 


If we adopt a historical attitude, then there is an extremely good answer, namely, Geometry. For approximately two thousand years, (Euclidean) geometry was taken to be the foundation of all mathematics. Numbers were regarded as lengths of line segments; quadratic equations were regarded as expressing the relationship of the areas of certain geometrical figures. All mathematics was, at bottom, geometric. Of course, there were problems with this. For many ancient mathematicians, for example, it made as little sense to add the cube of a number to its square as it would to add a volume to an area. The equals sign was not introduced until 1557, and it is easy for contemporary mathematicians to lose sight of how differently the ancients thought about the mathematical objects they studied and wrote about. Newton, famously, was so great a mathematician that he was able to introduce the differential calculus in terms of the ancient geometrical reasoning, although we rarely conceive of his ideas that way today. Indeed, much of this kind of writing now appears alien to us. 


Type theories form another class of foundations for mathematics, and are used in various places. For example, MartinLöf type theory is a constructive foundation of mathematics, and a lot of constructive mathematics has been formulated in it. Type theories are used in some proof assistants, like Coq, and they have nice connections with various programming languages in computer science  look up languages with dependent types. I should also mention that type theories have a close relation with categories  "Introduction to higher order categorical logic" by Lambek and Scott connects various type theories and categories. 


Arithmetic can be used as a foundation for a surprising amount of mathematics. The book Subsystems of SecondOrder Arithmetic by Steve Simpson demonstrates that a huge fraction of mathematics can be formalized arithmetically. In fact, firstorder Peano arithmetic suffices for most "ordinary" mathematics. I should point out, however, that even when using arithmetic axioms as one's ultimate foundation, people in practice formalize everything in (finitary) set theory first, and then show how to encode finite sets as integers. Set theory is just so darn convenient as a unifying language that it's hard to get away from it entirely. However, as long as you're really only dealing with finite or countable sets, almost anything you want to state and prove can in principle be done with integers, so in this sense arithmetic can be used as a foundation for most of mathematics. Areas of mathematics that are "intrinsically uncountable" cannot be captured by any of the systems in Simpson's book, but there are fewer of these areas than you might think. 


This was going to be a comment to Joel David Hamkins's answer on geometry, but it didn't fit. +1 This is one of the most clearminded things I have read on MO. It does not make a mockery of Foundations and still says something nonobvious. I'm very skeptical of all this business with category theory being a foundation for mathematics. First, whenever anyone talks about it, it always seems to be somebody else's work. It's become something of a meme that "Bill Lawvere has proposals to provide foundations for math through category theory", but we don't ever see details provided. Second, are we really to understand that we are going to add small integers with arrows and diagrams? Draw circles and lines, and say that the latter meet at most once? I think people work in transEuclidean hyperschemes of infinite type so much, they forget that math includes these things. As Wittgenstein remarks in the Investigations, just because you can express A in terms of B, it does not mean that B actually underlies A. 


I believe the lambda calculus was originally intended as a foundation for mathematics. More recently it seems that both category theory and type theory seem to be gaining support. Although, I think type theory (a la MartilLöf) could be viewed as another variation on the settheoretic theme. 


Von Neumann wrote down a foundation where the basic objects are functions, not sets. But it was soon recast into an equivalent system with sets (and classes). 


To follow up further on Joel David Hamkins's answer on geometry, Frege’s last work (two despairing decades after Russell’s Paradox demolished his Grundgesetze der Arithmetik) was a brief unpublished paper entitled “Neuer Versuch der Grundlegun der Arithmetik,” based on geometry with “the final goal, the general complex numbers.” (As in the Grundgesetze, he emphasizes that real numbers are ratios of quantities, not quantities themselves.) 


This may not satisfy the request for something that is "not, in any sense, a set theory" but Oliver Deiser has worked out two versions of foundations, one based on lists and one on multisets. This is in his book "Orte, Listen, Aggregate" (and his Habilitationsschrift with the same title). 


I know from the logical end there is plural quantification developed and expounded to some extent by Boolos, Lewis and others that sidesteps the whole issue of set and gives first order logic the ability to talk about setlike objects without resorting to set theory. 

