I'm quite surprised intuitionism is not brought into this conversation.
> Intuitionism is a philosophy of mathematics that was introduced by the Dutch mathematician L.E.J. Brouwer (1881–1966). Intuitionism is based on the idea that mathematics is a creation of the mind. The truth of a mathematical statement can only be conceived via a mental construction that proves it to be true, and the communication between mathematicians only serves as a means to create the same mental process in different minds. [^0]
The intuitionistic logic, through Curry-Howard-Lambek correspondence, serves an important role in proof theory and model theory.