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

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

Piotr,

>At the risk of sounding as a complete ignoramus:
>
>	Why do people bother with various type theories
>	when set theory is available?  What is the expected
>	gain?

I guess the answer is that it's more philosophically
attractive to them.  It's "the right way to construct
mathematics".  Or something like that.

Also, it's much closer to functional programming.  Maybe
they like functional programming?  In type theory you can
"execute" your mathematics like a program, which some people
seem to like.

Of course Mizar also has a type system, so the gain of
having _types_ should be clear to everyone.

However, having a type system and basing your mathematics on
type theory is not the same thing.  (Even the foundations
of HOL, which also consist of typed lambda calculus, does
not count as "type theory" I think.)

There is a very nice paper by Peter Aczel called "On
relating type theories and set theories", which shows how
both worlds correspond to each other.  So maybe in the end
it's the same thing :-)

Although of course _classical_ set theory does not correspond
to _intuitionistic_ type theories.  So I'd like to pose my
own version of your question here:

	Why do people bother with intuitionistic mathematics
	when classical mathematics is available?  What is
	the expected gain?

:-)

Freek