[FOM] formal proofs

[Freek Wiedijk]

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" :-))

Freek