[umanwizard]

Sure, but it fits the rest of mathematics "poorly" for exactly the same reasons. No working mathematician is thinking about 3 as an element of 5.

The reason ZFC is used isn't because it's a particularly pedagogical way of describing any branch of math (whether CS or otherwise), but because the axioms are elegantly minimal and parsimonious.

[k_bx]

Sorry but if you try to prove 2+2=4 in ZFC versus Type Theory (HoTT-style) – nothing looks elegant about ZFC afterwards.