principia

principia is a language and a system for documenting formal mathematics,
subject to syntactic and semantic conditions and structure.
All expressions are checked for syntactic
correctness, thereby eliminating a primary source of errors.
Mathematical syntax errors are highlighted just like spelling errors.
Principia is a strictly-typed
multi-sort object-oriented first-order language
with overloading, single-inheritance
and parameterised-types, that is rich enough to express
formal set-theory (which is elementary but with a definite description operator).
Principia integrates naturally with Latex, via a Latex package called PriTeX,
and the learning curve from LaTeX to Principia is small.
Principia is easier and more natural to write than LaTeX,
providing an environment facilitating ``thinking at the keyboard''.