>I think a discussion of types is especially relevant to the QED
>business. It seems to me that one of the many reasons that QED-like
>projects don't catch on more is that the world is so divided between
>those who love types (both those from a programming language
>background and also the followers of de Bruijn and Martin-Lof) and
>those who have no use for types (largely those with an upbringing in
>set theory as a foundation for mathematics).
In my humble opinion, the main reason why QED-like projects don't
catch on more is that most of them prefer formalizing mathematics
to doing something "useful", ie, something that a commercial company
is potentially willing to pay serious money for. It seems to me that
"real" engineers in the "real" world can't care less about whether
his or her tool is based on set theory or type theory, as long as
it can get his or her job done with minimum effort. The debate of
whether one should use set theory or type theory sounds to me a bit
like the debate of whether one should use C or Pascal.
Cheers,
- Ching Tsun