The design goal of semantic latex markup would be to decorate
existing formulas with type information. This would greatly benefit
computational mathematics. A single formula would be explicit
about its domain and range. Indeed, a single formula might have
more general form over C than over R, for example. Semantic
markup would result in multiple versions of the same formula.
Assumptions, such as branch cuts, could be made explicit and
available to the community. This might not set a standard but it might
encourage machinery to handle different decisions explicitly.
Provisos, such as limitations on the range (x in [1,2]), would be made
available for things like cylindrical algebraic decomposition (CAD)
algorithms.
The CRC and NIST collections with semantic markup would create
a "computer algebra test suite" (CATS) that all of the systems could
use as a reference.
Pattern matching systems, such as Albert Rich's RUBI matcher or
Richard Fateman's TILU would have much more information on
which to base patterns.
============
Consideration 0: Where are semantics inserted?
A search of the TeX package name space shows that selatex is unused.
This allows \usepackage{selatex} without conflict.
Axiom has 1177 categories/domains/packages (hereafter just called 'types'
except when being more specific).