Use of Mathematical Induction in Proofs of Program Correctness

Robert Floyd introduced MI as a systematic method to prove the correctness of computer programs in his 1967 paper "Assigning Meanings to Programs", written at the then Carnegie Institute of Technology, supported by DARPA.

This directly inspired Tony Hoare's axiomatic semantics and the development of Hoare logic (also known as Floyd-Hoare logic).

Floyd acknowledges gestation of these ideas by Perlis and Gorm, albeit in unpublished papers.