Constructive mathematics, Church's Thesis, and free choice sequences

We see the defining properties of constructive mathematics as being the proof interpretation of the logical connectives and the definition of function as rule or method. We sketch the development of intuitionist type theory as an alternative to set theory. We note that the axiom of choice is constructively valid for types, but not for sets. We see the theory of types, in which proofs are directly algorithmic, as a more natural setting for constructive mathematics than set theories like IZF. Church’s thesis provides an objective definition of effective computability. It cannot be proved mathematically because it is a conjecture about what kinds of mechanisms are physically possible, for which we have scientific evidence but not proof. We consider the idea of free choice sequences and argue that they do not undermine Church’s Thesis.