Dana Scott

Dana Stewart Scott (born 1932) is one of the rare people who reshaped two different corners of computer science — and won a Turing Award for the first before starting the second. With Michael Rabin he invented the nondeterministic finite automaton, the little "guessing" machine at the heart of every scanner; then, a decade later, he built the mathematical universe — domain theory — that finally gave programming languages a rigorous meaning.

Two careers, one Turing Award (so far)

In 1959, Scott and Rabin wrote a short paper, Finite Automata and Their Decision Problems, that casually introduced nondeterminism — the idea that a machine might follow several paths at once and accept if any succeeds. It sounds like cheating, and the beautiful punchline is that it isn't: the subset construction shows every nondeterministic machine has a deterministic twin. That paper earned the two of them the 1976 Turing Award.

But Scott was just getting started. In 1969, working with the Oxford visionary Christopher Strachey, he cracked a problem that had stumped everyone: how do you give a meaning to a program that can loop forever, or to the untyped lambda calculus where a function can be applied to itself? His answer was to invent domains — ordered spaces with a special "undefined" element \bot — in which recursion is simply a least fixed point. This is the foundation of all denotational semantics.

The model everyone said couldn't exist

There's a lovely twist. For years, logicians believed the untyped lambda calculus had no mathematical model — a set can't be the same size as the set of all functions from itself to itself, so "everything is a function that eats functions" looked hopeless. Scott's insight was to stop asking for all functions and keep only the continuous ones. Suddenly a space D \cong (D \to D) exists after all. He reportedly set out to disprove that a model could exist — and ended up constructing one instead, the famous D_\infty. A career highlight built on a failed refutation.

Scott and Strachey's slogan was that a program should denote a mathematical object — a function from inputs to outputs — computed compositionally from the meanings of its parts. A while-loop denotes the least fixed point of the function describing one iteration; a term that loops forever denotes \bot, "undefined". The radical part is that this meaning is completely independent of any machine, compiler, or clock. Decades later the same fixed-point machinery powers program verification, abstract interpretation in optimising compilers, and the semantics of lazy languages. Not bad for a theory that began as "let's be honest about infinity".

Beyond automata and domains, Scott has left fingerprints on modal logic (Scott–Montague semantics), set theory (Scott–Potter foundations), and constructive mathematics. He taught at Princeton, Oxford, Carnegie Mellon and elsewhere, mentoring a generation of logicians and computer scientists. His trademark is a certain mathematical taste: finding the one definition that makes a whole muddle click into place — nondeterminism for automata, continuity for semantics. Ideas that now feel inevitable were, once, just Dana Scott noticing what everyone else had missed.