Most of you probably heard about ZFC, this formal theory of sets from the early 20th that is said to be the fundamental language for modern math. Much rarer are the mathematicians that actually make use of it! Since the introduction of ZFC, formal logic has evolved a lot and since several decades other formal systems, more general (some would say more useful!) have been brought up. I will try to introduce the motivations for constructive systems, the links with computation, and demystify the law of excluded middle.