[...] but we have no guarantee at all that our formal system contains the full empirical or quasi-empirical stuff in which we are really interested and with which we dealt in the informal theory. There is no formal criterion as to the correctness of formalization.

-- Imre Lakatos, "What Does a Mathematical Proof Prove?"

ETA: When I first read this remark, I couldn't decide whether it was terrifying, or just a very abstract specification of a deep technical problem. I currently think it's both of those things.