Re: [mizar] [gmane.comp.science.types.announce] [Agda] CFP: Dependently Typed Programming (FI Special Issue)

[Freek Wiedijk <freek@cs.ru.nl>]

Bob:

>The type theories of folks like Martin Lof, de Bruijn,
>and Gerard Huet are even constructive.

FWIW: de Bruijn's system is not a type theory.  It's closer
to the logical framework "LF".  In such a system you
don't have _any_ foundations (constructive or classical)
from the start.  Instead you start by defining your logic
("axiomatically"), and only then start working on your
mathematics.  De Bruijn himself compares it to a restaurant,
where you can order different kinds of food.  I think.

Henk Barendregt once had a nice analogy, that unfortunately
I don't remember the details.  In it type theory was
intuitionism, set theory was Platonism, and de Bruijn-style
logical frameworks were formalism.  Or something like that.

Freek