{\huge Lint For Math}

Can we remove simple errors from math proofs? \vspace{1in}

Stephen Johnson is one of the world's top programmers. Top programmers are inherently lazy: they prefer to build tools rather than write code. This led Steve to create some of great software tools that made UNIX so powerful, especially in the ``early days.''

Today I want to talk about one of his tools, called }.

Steve was also famous for this saying about an operating system for IBM mainframes named TSO which some of us were unlucky enough to need to use: Using TSO is like kicking a dead whale down the beach. Hector Garcia-Molina told me a story about using TSO at Princeton years before I arrived there. One day he wrote a program that was submitted to the mainframe. While Hector was waiting for it to run he noticed that it contained a loop that would never stop, and worse the loop had a print statement in it. So the program would run forever and print out junk forever. Yet Hector, because of the nature of TSO, could not kill the program. Hector went to the system people to ask them to kill his program. They answered that they could not kill it until it started to run. Even better: the program would not run until that evening---do not ask why. So they could not kill it. But the evening crew could once it started. So they left a handwritten note to kill Hector's program later that night. A whale indeed.

Lint

Steve's lint program took your C program, looked at it, and flagged code that looked suspicious. The brilliant insight was that lint had no idea what you were really doing, but some constructs were likely to be bugs. These were flagged and often lint was right. A beautiful idea.

For example, consider the following simple C fragment: while(x=y) { ... } This is legal C code. But, it is most likely an error. The programmer probably meant to write: while(x==y) { ... } Recall in C the test for equality is $latex {x==y}&fg=000000$ while $latex {x=y}&fg=000000$ is the assignment of $latex {y}&fg=000000$ to $latex {x}&fg=000000$. The former could be correct yet it is likely a mistake. These are exactly the type of simple things that lint could flag.

The lint program has changed over the years and now there are more powerful tools that can flag suspicious usage in software written in any computer language. It was originally developed by Steve in 1977 and described in a paper ``Lint, a C program checker'' (Computer Science Technical Report 65, Bell Laboratories, 1978).

Lint For Math

I believe that we could build a lint for math that would do what Steve's lint did for C code: flag suspicious constructs. Perhaps this already exists---please let me know if it does. But assuming it does not, I think even a tool that could catch very simple mistakes could be quite useful.

There is lots of research on mechanical proof systems. There is lots of interest in proving important theorems in formal languages so they can be checked. See this and this for some examples. Yet the vast majority of math is only checked by people. I think this is fine, even essential, but a lint program that at least caught simple errors would be of great use.

Let me give three types of constructs that it could catch. I assume that our lint would take in a LaTeX file and output warnings.

$latex {\bullet}&fg=000000$ Unused variables. Consider

$latex \displaystyle \sum_{k=1}^{n} \frac{1}{i^{2}}. &fg=000000$

$latex \displaystyle \sum_{k=1}^{n} \frac{1}{k^{2}}. &fg=000000$

$latex {\bullet}&fg=000000$ Unbound variables. Consider

$latex \displaystyle T(n) = T(n-1) + T(n/2). &fg=000000$

$latex {\bullet}&fg=000000$ Under-constrained variables. Consider the statement,

For some $latex {c}&fg=000000$ it follows that $latex {T(n) \ge cn^{2}}&fg=000000$.

The statement may be technically true when $latex {c < 0}&fg=000000$, but for purpose of clear communication it needs a qualifier that $latex {c > 0}&fg=000000$. Perhaps the writer wrote that $latex {c}&fg=000000$ stands for a positive real number some pages earlier---we would not expect lint to pick that up. But we could reasonably ask lint to check for a mention of ``$latex {c}&fg=000000$'' in a previous formula and/or paragraph.

The TextLint applet page hosted by Lukas Renggli with Fabrizio Perin and Jorge Ressia does not flag the unused-variable condition, and evidently does not try to handle the other two situations. It also fails to catch '2\^{}16' which will give $latex {2^16}&fg=000000$ not the undoubtedly-intended $latex {2^{16}}&fg=000000$. This is more a LaTeX syntax issue than the kind of math-semantics error we are gunning for; the programs mentioned here also seem limited to this level.

Open Problems

Does a lint program like this already exist? If not should be we build one?