https://en.wikipedia.org/wiki/Intuitionistic_logic https://en.wikipedia.org/wiki/Intuitionistic_logic If you are familiar with "Classical" logic, constructive

https://en.wikipedia.org/wiki/Intuitionistic_logic https://en.wikipedia.org/wiki/Intuitionistic_logic If you are familiar with "Classical" logic, constructive math omits the law of excluded middle (e.g. "A or not A" must be true). In ZFC, the axiom of choice is omitted. This leads to proofs that are not only a verification of some idea but also gives you the mechanism to compute the evidence. This is often described as "the computational content of proofs" and is especially valuable in the context of the Curry-Howard isomorphism: for every proof, there is a corresponding program (and vice-versa). This is the basis for formal verification of constructive proofs. When creating a proof in Coq, you are actually writing the corresponding program. And you can even extract the program in another general purpose programming language (usually OCaml in the context of Coq, but Haskell is also supported).