Sources

The pull-quote in the article ("The programmer should make a number of definite assertions which can be checked individually, and from which the correctness of the whole program easily follows.") is from page 67 of the conference proceedings. The paper as a whole introduces three ideas at once: (1) assertions on arcs: attach propositions to each connection in a flowchart so checking a global property reduces to a finite set of local checks; (2) inductive variables: identify quantities whose value across iterations is captured by the assertion at the loop head; (3) variant functions for termination: attach a quantity to each loop that strictly decreases and is bounded below, so partial correctness can be separated from a termination argument. The worked example is a factorial routine implemented in addition only.

Turing describes the technique in the language of his audience (1949 hardware programmers writing for EDSAC and similar machines) rather than in modern proof-theoretic vocabulary, which is part of why the technique sat dormant for so long: the paper does not look like a "proof" to a 1960s reader trained on formal logic.

Cliff Jones, half of the Morris and Jones 1984 reprint team, returned to Turing 1949 in a 2013 chapter for the Cooper and van Leeuwen volume Alan Turing: His Work and Impact. The chapter walks through Turing's flowchart, his assertions, and his variant function using contemporary verification vocabulary, and is the most accessible "what is in the 1949 paper, explained from a modern standpoint" pointer for a reader who finds the original proceedings text and the Morris and Jones commentary heavy going. Jones also confirms the dating and circumstances of the EDSAC conference, and gives his own retrospective on why the technique did not catch on at the time.

Robert Floyd's Assigning Meanings to Programs is the paper that the verification community usually credits as the origin of inductive assertion methods. Floyd attaches propositions to the arcs of a flowchart, defines verification as showing that each node preserves its incoming assertion, and gives a termination argument based on a well-founded ordering. The structural similarity to Turing's 1949 construction is striking once the two papers are placed side by side, which is exactly what Morris and Jones do in their 1984 reprint. Floyd does not cite Turing 1949. Eighteen years separate the two papers.

The "Floyd had never heard of it" framing in the article's lead is the strong reading of two converging pieces of evidence. The conservative reading, taken directly from the published sources, is that no one has produced evidence that Floyd was aware of Turing 1949 when he wrote his paper, and that Hoare's own retrospective groups the two of them together as having independently rediscovered the technique. See the deeper annotation under the "unaware" finding below.

Hoare's An Axiomatic Basis for Computer Programming introduces the notation {P} S {Q} (precondition, statement, postcondition) and a set of inference rules for reasoning about it. The framing is more formally logical than Floyd's flowchart-based reading, but the underlying object is the same: a program annotated with claims whose preservation at each step entails the overall claim. As with Floyd 1967, the paper does not cite Turing 1949.

Dijkstra's Guarded Commands, Nondeterminacy and Formal Derivation of Programs takes the same logical material and rewrites it as a predicate-transformer calculus: for each program construct, the weakest precondition that guarantees a given postcondition is computed mechanically. This is the third independent statement of the verification idea Turing introduced in 1949: a different surface presentation (predicate transformers instead of flowchart annotations or Hoare triples), but the same load-bearing claim that program correctness is a property to be derived, not a property to be sampled by testing.

This is the article's most surprising historical claim, so it is worth setting out the citation walk in full. The published evidence comes from two sources:

1. Morris and Jones 1984, in the closing paragraphs of the IEEE Annals reprint, write: "In spite of the early date of Turing's paper and the insight shown, we know of no evidence that the paper influenced the later contributors to the ideas of program proofs." This is a careful statement: it says no influence has been documented, not that Floyd and Hoare were demonstrably unaware. It is the strongest claim a historian can make from the absence of citation alone.
2. Hoare 2003, in his own retrospective Assertions: A Personal Perspective, treats Turing 1949 as a separate ancestor that he and Floyd did not draw from at the time. The retrospective acknowledges the paper explicitly as the earliest known instance of the assertion technique, and groups his own 1969 paper with Floyd 1967 as later independent statements of the same idea.

A separate strand of evidence comes from the ACM Hoare Turing Award acknowledgements, which describe the 1949 paper as one "of which neither Floyd nor Hoare was aware in the 1960s." The conservative phrasing the article could use is therefore "was unaware" rather than "had never heard of it"; the published record supports the former precisely and the latter as a reasonable popular gloss.

By 1984 the verification community had three independent formalisms (Floyd, Hoare, Dijkstra) and a growing body of mechanized proof systems. Morris and Jones noticed that Turing's 1949 paper had said the same thing first, found the original proceedings, corrected the typographical errors that had made it hard to read, and reprinted the entire text in IEEE Annals of the History of Computing alongside a substantial commentary. The IEEE Annals version is now the standard citation for the paper, both because the proceedings are difficult to obtain and because the Morris and Jones corrections make the technical content followable.

This article uses the Morris and Jones commentary as its main secondary source for any claim about what Turing 1949 actually says, in preference to working from the proceedings text directly.

Hoare 2003 is the strongest piece of evidence the article uses for the claim that the verification community has now formally recovered the lineage back to Turing 1949. The retrospective is written by the person whose own name is on one of the rediscoveries; it explicitly identifies Turing 1949 as the precursor; and it does so without claiming awareness of the paper at the time the rediscovery was made. It is the cleanest acknowledgement available, and the closest the published literature comes to settling the "had never heard of it" question on its own terms. Paired with Morris and Jones 1984, it forms the two-source basis for everything the article says about the long silence and the eventual rediscovery.

The INRIA Toccata gallery hosts a working Why3 mechanization of Turing's 1949 factorial routine. The mechanized proof reproduces the flowchart structure, attaches the inductive assertions Turing wrote on the arcs, and discharges the verification conditions through an SMT solver. Parallel exercises exist in Coq, Isabelle/HOL, and Lean. The pedagogical value of the Toccata mechanization is that it makes the underlying logic of the 1949 paper concrete: the assertions become Why3 invariants, the variant becomes a Why3 variant clause, and the proof obligations that fall out are exactly the local checks Turing described in prose.

Martin Campbell-Kelly's EDSAC simulator at the University of Warwick is the standard pedagogical artefact for the 1949 machine. The site distributes a Windows-native simulator, an initial-orders bootstrap loader, a tutorial that walks the user through assembling a routine in the original notation, and scans of the contemporary programming literature. For a reader who wants to understand what Turing's "routine" actually looked like in storage, what it took to load it onto paper tape, and how the operator interacted with the machine, this is the working resource.

The simulator's documentation is also the proximate source for the Cambridge anniversary material below: the Warwick Links page is the only place on the open web where the EDSAC99 commemorative site is still being actively pointed at.

The Cambridge Computer Laboratory hosted a two-day event on 15-16 April 1999 to mark fifty years since the machine first ran. The commemorative site preserves the programme, the souvenir booklet, statistics from the original installation, archival reminiscences from people who used the machine in its working life, and a separate page indexing surviving EDSAC simulators. It is the closest the web has to a single-stop primary-source archive for the 1949 conference setting that frames Turing's paper.

The Computer Laboratory's "Relics" archive collects photographs of EDSAC and its operating environment, with captions identifying the people, the year, and the equipment in each image. Useful when an article needs to ground a sentence about "an operator reading off a cathode-ray display" or "the inaugural EDSAC conference" in an actual photograph rather than a sketch.

John von Neumann's First Draft of a Report on the EDVAC, circulated in June 1945 while von Neumann was consulting on the EDVAC project at the Moore School in Philadelphia, is the canonical written proposal for the stored-program computer. The report argues that program instructions should live in the same memory as data, so the machine can read, execute, and modify them through the same hardware paths. Every machine the article discusses (Manchester Baby, Mark 1, EDSAC, EDVAC) implements this proposal. Before it, programming meant physically configuring the machine: routing patch cables on ENIAC, setting plugboards on Colossus, punching paper tape for the Harvard Mark I. The First Draft is the moment "software" becomes a possible category of thing.

The Small-Scale Experimental Machine at Manchester, known as the Baby, executed its first stored program on 21 June 1948, eleven months before EDSAC. The program was Tom Kilburn's 52-instruction routine to find the highest proper divisor of a number, and its execution is the moment when the stored-program proposal in the EDVAC First Draft became a physical fact. The Baby's successor, the Manchester Mark 1, was the machine Turing was working on as deputy director when he came south to Cambridge to read his paper at the EDSAC conference. Useful context for an article that names EDSAC: EDSAC is not the first computer that ran software, it is the third or fourth, and the first to provide a regular computing service.