Home

MathLang

MathLang is next to what the name suggest: a mathematical language, also a framework for writing mathematical texts. It allows for more formalisation than the normal Common Mathematical Language does in such a way that one can check the correctness of the text (on some given level) but also convert it to even more stringent forms so that it can be checked by proof checkers such as (Mizar, Coq, PVS, etc.).
By Jim Apple at 2006-05-09 03:46 | DSL | other blogs | 9655 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Why not J?

APL was originally a redesign of mathematical notation with computers in mind. J takes that to the next level. Even if you know nothing of J, you can work through Ken Iverson's texts that use it (e.g., "Math for the Layman"). I wish J had been available when I was in college (of course now people use Mathematica for that sort of thing).

(J is not perfect. It quickly drives me crazy when I try to use it to write applications. J shines for experimenting with ideas.)

By James Hague at Tue, 2006-05-09 13:55 | login or register to post comments

How is J in the bounds specified?

It's not clear to me that J makes an attempt at the goals of this project, not just to be a mathematical language, but to allow "more formalisation ... in such a way that one can check the correctness of the text (on some given level) but also convert it to even more stringent forms"

By Jim Apple at Wed, 2006-05-10 02:20 | login or register to post comments

J is great but...

I still miss APL from the short period when I programmed in it 20 years ago. But APL and J are nothing like what is needed for a general purpose mathematical language. They are excellent for a compact notation to describe many types of operations on arrays or array-like structures. But the universe of mathematics contains a wide variety of objects - sets, classes, propositions, topological spaces, categories, and so on. In fact, "Math for the Layman" suspiciously seems to have a bias towards those branches of mathematics that involve arrays.

By sigfpe at Tue, 2006-05-09 16:35 | login or register to post comments

Comapre

With this.

By Ehud Lamm at Wed, 2006-05-10 10:05 | login or register to post comments

Very different

I would suggest reading over these (PDF) slides for a better overview of MathLang. To me this seems quite different from POPLMark. POPLMark aims to be fully formal in the restricted field of programming language meta-theory, no matter how much pain that inflicts on the writer, while MathLang hopes to be just formal enough to be as correct as current mathematics, but also trying to minimize the pain to the writer, yet covering a much wider field.

MathLang's deep pragmatism is much more reflective of de Bruijn's Mathematical Vernacular than of any current approach to formalization. Current approaches stress "formal", while pragmatism seems to be an unknown concept. This is an understandable over-reaction to current informality, but I am patiently waiting for concerns of usability to make some inroads in current approaches before I dive in too far.

By Jacques Carette at Wed, 2006-05-10 16:59 | login or register to post comments

big ideas

Nice, I thought about something like that the other day - I bet that the big thing in this area could be

1. getting this integrated into a WYSIWIG math text editor, so that writing mathematical text would be easier and funnier
- including authomatic refactoring of formulas and equation is big here

2. putting there enough mathematical knowledge to handle secondary-school olympic mathematic problems,
- so as to attract young students to a sort of competition and training website, sort of "TopProver", that way it could gain significant popularity

By Marcin Stefaniak at Sun, 2006-05-14 11:00 | login or register to post comments