[lmm]

> And yet, the current mathematics relies heavily on the ZFC set theory. Why is that ? (Is that assumption even correct ?)

Not really. Most working mathematics is done without any particular foundational context (in fact, it's probably done in naive set theory). If you asked a mathematician, they'd tell you they were using ZFC, but only because everyone does; in practice they don't know or care what foundations they're working with.

> From what I've learned so far, the set theory suffers from Russel's Paradox[0] (does the set of all sets that does not contain itself, contains itself ?). That's what motivated the formalization of Type Theory and the invention of Type Systems in programming languages.

Naive set theory suffers from that paradox. ZFC is a minimal "patch" that avoids it (through the rather ugly hack of an axiom schema).

It shouldn't surprise any programmer that most people working in the field would rather use a bodge that lets them use all their existing theorems and avoid having to learn anything new, rather than a new foundational paradigm.

People who care deeply about foundations are working on things like HoTT. But it's just not that important to day-to-day working mathematicians.