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

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

All,

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 have been asking this question for years and never got a convincing answer.


Cheers, PR


On Wed, Jul 02, 2008 at 10:37:42PM +0200, Josef Urban wrote:
> 
> Hi Jesse,
> 
> >This may be somewhat inappropriate for mizar-forum, but it seems
> >noteworthy to me that in the non-exhaustive list of systems for
> >dependent types mentioned in this recent post to the TYPES forum, mizar
> >is not mentioned.  Would it be appropriate to write an article on
> >mizar's dependent types for the upcoming special issue of Fundamenta
> >Informaticae?  One initial question to consider: does mizar's type
> >system differ in any interesting way from the type sytems mentioned
> >below?
> 
> I think the reason why the Mizar type system is not mentioned is that 
> people know very little about it. And it seems to me that there is 
> practically no research being done on Mizar type system, even though it is 
> a very "practical" and notrivial thing to have good "type" automation over 
> set theory. And yes, Mizar's type system significantly differs from 
> others. So I think it is a very good idea to do more research and publish 
> about it.
> 
> Josef

-- 
Piotr Rudnicki                                http://web.cs.ualberta.ca/~piotr