One thing to note is that theorem provers/proof assistants like Coq and Agda are based on constructive mathematical foundations (calculus of constructions). Typ

One thing to note is that theorem provers/proof assistants like Coq and Agda are based on constructive mathematical foundations (calculus of constructions). Type theory (related to types in programming languages, lambda calculus is one potential example) is also fundamentally constructive.