Cherry & Kernighan's eqn (the formula-handling part of troff) was written in 1974, while I think that Tex wasn't distributed much until the early 1980s. Eqn is still used, but not by mathematicians that I know of. It's not really what psihodelia was after, but I'd be curious to hear of mathematicians using eqn in the 1970s.

+1 Very good point. It's worth pointing out that Willard's system does express multiplication in terms of division, as a relation, but it fails to prove the multiplication relation expresses a total function, although all and only the expected constant instances are true. Since Willard's system thereby has the same prime numbers as usual arithmetic, and has their primality as theorems, we have the converse to Joel's point: presence of (a weak theory of) primes together with completeness.

@Sergei: The core should be a simple, easy to understand algorithm, but that does not mean it needs to be computationally trivial or inexpensive. I am not sure, but I think that proof checking for both LF and Gallina (Coq's core logic) are EXPTIME problems.

@Sergei: Q1: often. Q2: when it comes to verification, the proof objects we are concerned with are usually text files that the user prepares, with or without the help of a proof editing assistant. These typically are, like Hilbert-style proofs, a list of assertions that build up to the conclusion, but typically there are gaps that the prover checks by performing some nontrivial (but usually decidable) computation to check.

svn is less attractive than distributed version control (DVC) for simultaneous editing: people shouldn't have to create branches to commit changes that haven't yet incorporated other people's edits. Generally authors and editors want to accept or reject other people's edits in a few at a time, while creating their own changes: DVC allows this, svn makes it hard.

You can add the links back in as regular text.

I have had good experiences using this in my editing work with clients. Latexdiff works well together with distributed version control, allowing two or more people to work on a document side-by-side. I'd love to see a latex3diff, to handle 3-way diffs.

mmverify's author is Raph Levien.

System T is stronger than primitive recursion: system T extends PRA by allowing recursors at all finite types, while PRA only allows them over the natural numbers. But yes, I agree and to emphasise: system T is the equational theory corresponding to PA, and defines just the functions that PA proves total.