[zomglings]

I'm confused why you would need the Axiom of Choice when working with computable programs.

Unless you were proving theorems about possible contents of a database? But even that seems like you wouldn't need the Axiom of Choice.

Could you elaborate on what you were doing with ZFC with databases?

[mr_gibbins]

Not to cop out but a HN reply isn't the best place to provide a full explanation. Suffice to say I use the ZF axioms as a basis to teach how sets both differ from and are similar to tables, particularly using the more accessible parts of Stoll's textbook on axiomatic set theory. To give a single example, the axiom schema of replacement is a good analogy for how the output of a SELECT command over a set will also result in a set.

In terms of AC, the comment below about how this is actually the AFC is correct, since the sets I am talking about are finite. Of course, set projections or selections are arguably choice functions themselves, which makes them relevant, and ZFC includes AC in order to infer well-orderedness, which tables (after all, collections of sets) can indeed be.