In defense of sets, I very much like them as a foundational concept, in considerable part because one can reach a larger audience by starting from sets than from sheaves. I was impressed that anyone would dislike sets so much as to compare starting from them to standing in wet concrete until it sets (or were you just making a pun about sets, Steve?).
No, I was in earnest. Having over quite a few years now seen for myself the possibilities of using constructive reasoning to _simplify_ mathematics, so that it now seems very obvious, I get overquickly distressed when other people still haven't seen it. However, I should explain that I was not criticizing sets as pedagogic foundations, where you start from when you're explaining to a large audience, nor as (if I may use Paul Taylor's phrase) practical foundations, since the naive concepts of sets (albeit non-classical ones) underly the way one reasons in toposes. The parable about concrete concerned philosophical foundations, trying to fix on classical set theory as the deep unifying account of what mathematics depends on. Maybe in any case Vaughan wasn't thinking so much about such philosophical diversions. There is a pragmatic message. There are a number of different characterizations of finiteness. Classically they are all equivalent, but it has been known to topos theorists for quite a while now that if you start considering non-classical sets (such as sheaves) or computational structures you find they are inequivalent. My belief is that the explanations of the differences can be understood in naive set theoretic terms, though to see why they are genuine differences and not just presentational you need to know a bit more about sheaves and such. A particular message (really arising out of geometric logic) is that finiteness is _structure_ on a set, and not just a property: How do you know a set is finite? There is something there in its structure that tells you. I've tried to bring this out in my paper "Strongly algebraic = SFP (topically)", soon to appear in Math. Structures in Computer Science, and also available through my web page http://mcs.open.ac.uk/sjv22. In particular you see there discussed Kuratowski finiteness (you can list of all the elements but can't necessarily remove duplicates), finite decidable (in addition you can detect inequality between elements and so can remove duplicates) and finite ordinals (there is a canonical list that thereby puts an ordering on the elements). Consequently, when giving (as Vaughan did) a categorical characterization of finiteness, it's worth pausing to consider which kind of finiteness you are characterizing. Some will be more fruitful than others in terms of how successfully they can generalize to the non-classical sets - with some you will be stuck in your concrete, with others you can explore further afield. The particular one Vaughan described was closely tied to the classical set theory, but that is a limitation that is not inherent in the broad questions he was asking. That's a bit more subtle than saying "finite sets" are now characterized, and treating "finite sheaves" as an interesting topic of further study along with "finite Abelian groups" and so on. There is virtue in finding answers for "finite sets" that also apply to "finite sheaves".
Mentioning categories on Steve Simpson's FOM mailing list typically brings on a diatribe from someone railing against categories. It would be nice if one could mention sets on this mailing list without the analogous response.
Sorry if I railed. The categories list has the big advantage that its readership is very well informed about both sets and categories, and fully in a position to base their opinions on the mathematics and not the railing. All the best, Steve Vickers.