[FOM] formal proofs

[Timothy Y. Chow]

On Tue, 28 Oct 2014, Bas Spitters wrote:
> A short remark. Feit-Thompson was proved in the calculus of inductive 
> constructions (Coq) and Flyspeck used HOL. Neither of them used ZFC and 
> computation was very important in both theorems. This is in line with 
> the development in HoTT.

Yes; perhaps I should have introduced not just a two-way distinction 
between "traditional foundations" and "HoTT foundations" but a three-way 
distinction between "traditional set-theoretic foundations," "traditional 
type-theoretic foundations" (including Coq and HOL) and "HoTT 
foundations"?  I thought that the claim was that HoTT was a radical 
improvement over both kinds of "traditional foundations," but maybe the 
main claim is just that type-theoretic foundations are a radical 
improvement over set-theoretic foundations?

Tim