Part of the problem here is the widespread acceptance of the notion that
one should start from a small set of axioms and deduction
rules and derive everything else from these elementary foundations.
In applied math, we often introduce notions and methods from the physical
world or mix and match from what logicians would regard as incommensurate
theories. The QED project should not require that working mathematicians
accept the strictures common in metamathematics.
Has anyone here read
Boute's essay: "A critique of the axiomatic method in computer science" ?