Who are the intended customers of QED?
The recent discussion seems to assume that mathematicians are
the intended customers. For instance, David McAllester wrote:
> Mathematicians are concerned with truth. From a marketing perspective
> it seems better to speak their language.
But are mathematicians really interested in something like QED? I am
not a mathematician, so I don't really know. But my impression is that
most mathematicians (logicians included!) are quite happy with informal
proofs and the social process of debugging such proofs. Furthermore,
it seems to me safe to assume that unless using a mechanical theorem
prover can be as easy as writing informal proofs, most mathematicians
will NOT be interested in something like QED. Unfortunately, as anyone
who has used a mechanical theorem prover knows, we don't have such
technologies yet. Is building such easy-to-use theorem provers a main
goal of QED?
Moreover, even if most mathematicians are interested in something like
QED, are they (collectively) willing and able to pay for it? I personally
don't think so, but again, I don't know as I am not a mathematician.
Shouldn't the QED community pay more attention to other potential
customers? Especially those who can PAY for it?
Cheers,
Ching-Tsun Chou