RE: [Axiom-developer] MathLang

[Page, Bill]

On Tuesday, July 18, 2006 8:32 AM C Y wrote:
> 
> Just saw an announcement on the Isabelle list
> (http://www.macs.hw.ac.uk/~jbw/phd-student-ad.html) which
> referenced this:
>
http://www.macs.hw.ac.uk/~fairouz/talks/talks2005/mathlang-general-talk.
pdf
> 
> I may be wrong, but it sounds like the problems they are
> looking at there are a bit similar to the ones B-sharp is
> intended to address.

It seems to me that goals of MathLang go way beyond BNatural
(B# or B-sharp if you prefer). BNatural is a single-typed input
language intended to replace or suppliment the existing Axiom
interpreter, especially for new users of Axiom. MathLang on
the other hand is apparently intended as a semi-formal middle
ground between published mathematical text and a formal input
language (such as BNatural, the Axiom Interpreter or an automated
theorem proving system). Maybe some day this will be a possible
input language for computer algebra systems, but it seems to me
that having just learned to crawl, we should first set our sites
on learning to walk before we try to run ... :)

Regards,
Bill Page.