The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Daniel Schepler wrote:
> But it's starting to sound like the theory you're formalizing is 
> possibly tied tightly enough with ZF-type semantics that using a ZF 
> system would indeed be appropriate.  I think Adam wasn't necessarily 
> saying that using a ZF system would automatically be a bad idea, just 
> that in most of mathematics outside pure set and model theory (and 
> even in quite a bit of set theory), it's more natural to formulate it 
> in type theoretic terms.

I'd put it this way: when some development is said to be doable in ZF 
but not CIC, I immediately doubt whether the development has practical 
value.  Not that there's anything wrong with impractical mathematics.... ;)