I just read that Hermann Weyl used a certain type of type theory as the foundation of mathematics in his book "The Continuum" and he was able to derive calculus without the use of infinite sets. Naturally, I'm going to read it ASAP but I wanted to ask right away what it's fundamental flaws are, since obviously its not taken as the conventional foundation (instead of ZFC). I'm inclined to assume that it's nothing detrimental to mathematical physics, since that was Weyl's primary field.
You can see Hermann Weyl:
In Das Kontinuum he tries to overcome this [the vicious circles he believed being involved with set-theoretical approach to foundations] by providing analysis with a predicative formulation — not, as Russell and Whitehead had attempted, by introducing a hierarchy of logically ramified types, which Weyl seems to have regarded as excessively complicated — but rather by confining the comprehension principle to formulas whose bound variables range over just the initial given entities (numbers). Accordingly he restricts analysis to what can be done in terms of natural numbers with the aid of three basic logical operations, together with the operation of substitution and the process of “iteration”, i.e., primitive recursion.
Weyl recognized that the effect of this restriction would be to render unprovable many of the central results of classical analysis — e.g., Dirichlet’s principle that any bounded set of real numbers has a least upper bound — but he was prepared to accept this as part of the price that must be paid for the security of mathematics.