Hacker News new | ask | show | jobs
by danidiaz 1548 days ago
A related answer in the CS Stack Exchange: https://cs.stackexchange.com/a/91345/5296

> type theory is not about syntax. It is a mathematical theory of constructions, just like set theory is a mathematical theory of collections. It just so happens that the usual presentations of type theory emphasize syntax, and consequently people end up thinking type theory is syntax. This is not the case.