Mike Gordon
A grouping.
Mike Gordon (1948--2017), at the Cambridge Computer Laboratory. Nine records, all from the open UCAM-CL-TR series, and together they are the most complete account the corpus holds of how one person built a method and then replaced it.
Read as two tool-and-demonstration pairs, three years apart:
TR-41 (1983) is LCF_LSM -- the LCF programming environment plus the Logic of Sequential Machines -- presented as both an overview and a user manual. TR-42 (1983) is Gordon's computer proved correct in it: 8 opcodes, 26 microinstructions, and an appendix deriving a hard-wired controller from a microprogram by machine-checked inference, which is formal synthesis six years before that name settles on it. Each report says it should be read with the other.
TR-68 (1985) is HOL, higher-order logic given "a machine oriented formulation" so a program can implement it; TR-103 (1987) is the HOL system rather than the logic -- an ML tutorial, tactics and tacticals, and a worked hardware example -- and its abstract names the ancestry the logic report does not: HOL is a version of Robin Milner's LCF. TR-100 (1986), with Joyce and Birtwistle, redoes the same computer in it. The second pair exists because the first was superseded, and the move it records -- from a calculus built for hardware to a general-purpose logic -- is the axis kumar1996formal makes the basis of its classification thirteen years later. One consequence visible across the pairs: LCF_LSM's verification relation is behavioural equivalence, where HOL permits implication with an abstraction function, which is what complex devices need.
Between the pairs sit the two reports that matter most to the-switch-or-the-curve. TR-77 (1985) argues the case for higher-order logic in hardware and, in doing so, defines the two-valued transistor model -- Pwr(p) = (p = T), Gnd(p) = (p = F), Ntran(g,a,b) = (g implies a = b) -- that Basin adopts at Cornell four years later. TR-91 (1986), with Camilleri and Melham, then refutes those definitions: connect power to ground and the circuit's formula becomes false, whereupon it "would correctly implement every specification". Their conclusion, "we need better models of transistors", is answered by Joyce the following year with four values.
TR-66 (1985), with John Herbert, is the one that pays. The ECL chip of the Cambridge Fast Ring, about 360 gates, verified through a purpose-built interface to the Cambridge Design Automation System's own design database -- so the thing proved was the thing the engineers were using. Errors were found, corrected, "and when the corrected design was eventually fabricated it was functionally correct first time".
What the corpus does not hold under his name it holds under his logic: Cohn's two VIPER reports, Joyce's four, Melham's book and Gammie's survey all rest on HOL. "Gordon's computer" is a benchmark rather than an example -- proved in LCF_LSM, in HOL, and later in OBJ3 by Stavridou.
TR-94 (1986), with Cohn, is the third of the group's controlled comparisons: RSRE used a simple counter to illustrate its own LCF_LSM-and-ELLA methods, and this redoes that counter in HOL. Its conclusions are the sharpest cost statement in the cluster -- more effort goes into writing and correcting the definitions than into the proofs, and four further formal specifications had to be invented before the RSRE descriptions could be proved about at all. It also records, in passing, that "details of VIPER are not in the public domain", which is the upstream condition for everything Cohn later reports about that chip.
Still missing from this cluster: nothing essential. The remaining Cambridge hardware reports are by others -- Herbert on the CFR ECL chip in HOL, Camilleri on simulation as an aid to verification.