Where Hilbert erred was looking for foundations in first-order logic. Univalent foundations are laid on high-order logic. It's the distinction between top-down

Where Hilbert erred was looking for foundations in first-order logic. Univalent foundations are laid on high-order logic. It's the distinction between top-down and bottom-up thinking. If you are into philosophy/epistemology - it's somewhat of an attempt to shift Mathematics from foundationalism towards structuralism. I recommend this video: https://www.youtube.com/watch?v=O45LaFsaqMA https://www.youtube.com/watch?v=O45LaFsaqMA Hilbert's dream of Metamathematics has sort of come true in the form of homoiconicity in programming languages.