"Literal Mathematics"

There seems to be a real revolution in mathematics on its way, namely the long due formal standardization.

This process is maybe best elaborated in this hierachy of three designs:

• MathML, now in version 3.0 (December 2009), an XML application with the basic sytax in two modes: Presentation Markup and Content Markup. [http://www.w3.org/TR/MathML]
  

• OpenMath, a standard for representing the semantics of mathematical objects. [http://www.openmath.org]
  

• OMDoc, for the formalization of entire documents. [http://www.omdoc.org]
  

Sure, in our times there is an inflation of revolutions. But I think, this one is a really big one, despite the unexciting appearance of any norm.

• A standard will provide us with a common language. A common language for mathematicians is more than a lingua franca or English as the world language. Formal scientist always need to create the world first, before they can talk about it. But at present, there is not even an agreement on whether "natural numbers" start from 0 or 1. This is not freedom, but pure inefficiency.

• Currently, each constructive idea requires a choice for a concrete programming language when it is implemented. "Higher" languages have an interface concept that abstracts the signature from the details of the implementation. But there are no real standards for the translation between different languages. Each language needs to re-implement all the libraries to be a useful one. Of course, there is XML now, and that is a big step (MathML, OpenMath, and OMDoc are XML, too). But for mathematical structures and theories, XML itself is all too general.

• This standardization of mathematics is not a new foundation in the meta-mathematical sense. It is a syntactic agreement, not a semantical super-theory. It doesn't explain, what a mathematical object really is, it only defines, how we define one. I suppose, this whole movement comes so late, because it was everything but obvious from the tradition, that a global standard does not need a global ontology. (And maybe in the end, that is a new foundation, after all.)

• Donald Knuth introduced literal programming as an emphasis on the idea that documents should be comprehensive for humans and computers alike. Many programming languages offer "literal programming" tools, but none of them complies to the promise.

Unfortunately, at present there is still a shortage of tools to efficiently and comfortably work with these new formats.