Stavros:
> > Why would you want to reimplement [Otter] rather than
> > interface to it as a black box?
CY pointed out some of the complications of interfacing to an external
package rather than translating it, but there is one huge complication
of translating rather than interfacing: you now have two sources rather
than one.
If you have two sources, then you must port any bug reports, test
suites, bug fixes, and enhancements from one to the other, one item at a
time. If of course the other package is no longer being maintained,
then this is irrelevant -- but in that case there is also no danger of
new incompatibilities.
Personally, I do always like to have source in Lisp because I am more
comfortable in the Lisp environment than any other one. But I should
learn to deal better with other systems. Oh, and systems in general
should learn to "play together" better -- Maxima of course being as bad
as other systems this way.
It is also not clear that a Lisp version of Otter would actually be
enhanced at all -- will we attract theorem-prover hackers to the Lisp
version? If we do want a Lisp-based theorem prover, perhaps it would be
better to find an existing one....
I also wonder how much of a performance hit one would get by moving from
C to Lisp. Theorem provers are slow, I think, so a factor of 5 or 10 or
50 in speed could make a real practical difference.
-s