In 1947 reports by [[John von Neumann|von Neumann]] and [[Herman Goldstine|Goldstine]]<ref>Goldstine and von Neumann. [https://library.ias.edu/files/pdfs/ecp/planningcodingof0103inst.pdf Goldstine and von Neumann "Planning and Coding of problems for an Electronic Computing Instrument"]. Part II, Volume I, 1 April 1947, p. 12].</ref> on their design for the [[IAS machine]], they described algorithms using an early version of [[Flowchart|flow charts]], in which they included assertions -: "It may be true, that whenever C actually reaches a certain point in the flow diagram, one or more bound variables will necessarily possess certain specified values, or possess certain properties, or satisfy certain properties with each other. Furthermore, we may, at such a point, indicate the validity of these limitations. For this reason we will denote each area in which the validity of such limitations is being asserted, by a special box, which we call an assertion box."
The assertional method for proving correctness of programs was advocated by [[Alan Turing]]. In a talk "Checking a Large Routine" at Cambridge, June 24, 1949 Turing suggested: "How can one check a large routine in the sense of making sure that it's right? In order that the man who checks may not have too difficult a task, 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".<ref>Alan Turing. [http://www.turingarchive.org/viewer/?id=462&title=01 Alan Turing, Checking a Large Routine], 1949; quoted in C. A. R. Hoare, "The Emperor's Old Clothes", 1980 Turing Award lecture].</ref>
