[FOM] formal proofs

[croux at andrew.cmu.edu]

> Dear Cody,
>
>>For instance, what foundational system would dream of
>>having a complex module system?  It seems redundant and
>>wasteful. However, any hope of having a practical system
>>needs to address this question.
>
> Really?  As will be clear, I really like HOL light,
> I think it's one of the best current systems for formal
> mathematics (e.g., it was used for the Flyspeck project).
> It certainly is a practical system.  Still, HOL Light has
> no module system whatsoever.  (And _certainly_ not in it's
> "foundational system" :-))
>
Right. The point I was trying to make is that formalization *in practice*
depends more on, say, the ability to overload notations (I should have
picked that example instead of modules!) than whether you are working in
ZFC or HOL.

Cody




> Freek
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>