It's a big question, this I am quite aware of, so please excuse my little understanding on the subject but with reference to the following question, to which I would rather like to extend a little, how does one go about demonstrating or expressing, mentally or visually "...ZFC has a model. Type theory is more like a programming language"?
I understand this may be a difficult task, considering so much has developed over the last few decades, logicism and its terminology has evolved and various concepts have come and gone.
It is quite evident to see - how transforming Type Theory really was, how one was able to pragmatically construct, with type theory itself, out of "pure logic" so to speak, a system, a unique foundation. I am trying to touch both the philosophical conceptions and the mathematical practicalities.
If there are any relevant answers or similar questions already, I apologise for my ignorance and if I have not articulated my question correctly I apologise for my lack of acute knowledge on the subject. I am just beginning my venture.