[FoRK] Axiom: symbolic mathematics language w/ rigorous mathematical types

Contempt for Meatheads jbone at place.org
Sat Jun 5 12:00:28 PDT 2004

 From the types-are-cool file...

Check this out:


Musing:  have been a Mathematica user for years;  have been intrigued 
by symbolic math systems since writing a little linear equation solver 
in Turbo Pascal back in high school (oh those many years ago...)  Most 
of the more mature math systems (like Mathematica) them are fully 
computationally expressive --- yet people generally don't build large 
software systems in them.  Why not?  I find the difference in treatment 
of unbound symbols in math languages vs. "regular" programming 
languages rather theoretically interesting, and have always wondered 
whether there's not a lurking concept there that could be usefully 
exploited vis-a-vis building large, robust  software systems.

Other side note:  looking at this and at Frink (posted last week, IIRC) 
I've started wondering whether there's a potential algebraic 
unification in a derivative typed lambda calculus between the concepts 
of multiplication, application, parametric type composition ala 
Haskell's monads.  Theory of computation as equation solving?



More information about the FoRK mailing list