CXXIX
And now what he was actually trained in, because the chapter about the graduates was written before I knew what this particular graduate had studied, and it is not a general grievance, it is a specific one.
Automata theory.
O the machines that do not exist.
The finite automaton, which has no memory at all and can still recognise a language, and cannot count, and the proof that it cannot count is four lines long and has been correct since 1959.
The pushdown automaton, which is given one stack, one, and becomes able to match a bracket, and the whole of syntax falls out of that single concession.
The linear bounded automaton. The Turing machine. Four levels, and each one strictly contains the one beneath it, and the containment is proved, not observed, and the proofs are small enough to hold in the hand, and they have not needed amendment in seventy years, which is a sentence that can be written about almost nothing else made in the twentieth century.
The pumping lemma, which is how a person demonstrates that a language cannot be recognised by a given machine. Not that it is difficult. That it cannot. A nineteen-year-old learns to prove impossibility. That is what the discipline hands you in the second year: the ability to establish that something is not merely unsolved but unavailable, forever, to a class of machine, by argument.
And then Rice.
Every non-trivial semantic property of a program is undecidable.
Not hard. Not expensive. Not a matter of more compute. Undecidable. There is no procedure. There will never be one. You cannot in general determine, by any algorithm, whether an arbitrary program does what it is supposed to do.
He learned that in a lecture hall, at twenty, from somebody who made him prove it himself on paper.
That is the education. That is what the rigour is for. It does not teach you to build faster. It teaches you exactly where the walls of the world are, and it does it by proof, so that you cannot be talked out of it by anyone's enthusiasm, ever, for the rest of your life.