Martin Escardo on Nostr: I am so glad there are so many clever people who study the syntax of *dependent* type ...
I am so glad there are so many clever people who study the syntax of *dependent* type theory.
This is a rather non-trivial subject, which is indispensable for e.g. making proof assistants work.
It is very tempting to think that syntax is such a concrete thing to the extent that it would be trivial to deal with it.
I know two mathematicians who told me literally this sentence to my face: "syntax is very abstract".
One would think that syntax is very concrete.
One of them was my former PhD student Ho Weng Kin, in 2003, and the other was Voevodsky in 2015 (in the last TLCA, which then became FSCD).
There are two aspects of (abstract) syntax.
(1) The mathematics needed to implement it in the computer.
(2) The mathematics needed to define what the models of syntax are, and then define the many models we are interested in. (For example, models of HoTT/UF should be \infty-toposes, but his is just one example.)
When developing proof assistants, we can ignore (2) but not (1).
But many people who use proof assistants are interested in (2).
I know about (2), and although I don't work in (1), I recognize the heroic achievements in (1).
This is a rather non-trivial subject, which is indispensable for e.g. making proof assistants work.
It is very tempting to think that syntax is such a concrete thing to the extent that it would be trivial to deal with it.
I know two mathematicians who told me literally this sentence to my face: "syntax is very abstract".
One would think that syntax is very concrete.
One of them was my former PhD student Ho Weng Kin, in 2003, and the other was Voevodsky in 2015 (in the last TLCA, which then became FSCD).
There are two aspects of (abstract) syntax.
(1) The mathematics needed to implement it in the computer.
(2) The mathematics needed to define what the models of syntax are, and then define the many models we are interested in. (For example, models of HoTT/UF should be \infty-toposes, but his is just one example.)
When developing proof assistants, we can ignore (2) but not (1).
But many people who use proof assistants are interested in (2).
I know about (2), and although I don't work in (1), I recognize the heroic achievements in (1).