This paper by C. A. R. Hoare explores the logical foundations of computer programming using axiomatic methods, a technique initially applied in geometry and later extended to other branches of mathematics. The author aims to elucidate sets of axioms and rules of inference that can be used to prove the properties of computer programs. Key topics include: 1. **Introduction**: Computer programming is treated as an exact science, where all properties and consequences of a program can be deduced from its text using valid rules of inference and axioms. 2. **Computer Arithmetic**: The properties of elementary operations like addition and multiplication of integers are crucial for valid reasoning about programs. The paper discusses the differences between computer arithmetic and traditional mathematical arithmetic, emphasizing the importance of selecting appropriate axioms. 3. **Program Execution**: The paper introduces axioms and rules of inference for program execution, including the Axiom of Assignment, Rules of Consequence, Rule of Composition, and Rule of Iteration. These axioms and rules are used to prove properties of simple programs, such as finding the quotient and remainder in division. 4. **General Reservations**: The axioms and rules assume the absence of side effects and do not address termination issues. The paper suggests adapting the axioms to handle nonterminating programs and highlights the need for more powerful proof techniques. 5. **Proofs of Program Correctness**: The most important property of a program is its correctness. The paper argues that proving program correctness can reduce the costs associated with programming errors and improve reliability, documentation, and compatibility. 6. **Formal Language Definition**: The paper discusses the use of axioms for defining the semantics of high-level programming languages, ensuring compatibility among different implementations and facilitating better language design. The author concludes that while program proving is currently challenging, it offers significant theoretical and practical advantages, particularly in reducing errors and improving reliability.This paper by C. A. R. Hoare explores the logical foundations of computer programming using axiomatic methods, a technique initially applied in geometry and later extended to other branches of mathematics. The author aims to elucidate sets of axioms and rules of inference that can be used to prove the properties of computer programs. Key topics include: 1. **Introduction**: Computer programming is treated as an exact science, where all properties and consequences of a program can be deduced from its text using valid rules of inference and axioms. 2. **Computer Arithmetic**: The properties of elementary operations like addition and multiplication of integers are crucial for valid reasoning about programs. The paper discusses the differences between computer arithmetic and traditional mathematical arithmetic, emphasizing the importance of selecting appropriate axioms. 3. **Program Execution**: The paper introduces axioms and rules of inference for program execution, including the Axiom of Assignment, Rules of Consequence, Rule of Composition, and Rule of Iteration. These axioms and rules are used to prove properties of simple programs, such as finding the quotient and remainder in division. 4. **General Reservations**: The axioms and rules assume the absence of side effects and do not address termination issues. The paper suggests adapting the axioms to handle nonterminating programs and highlights the need for more powerful proof techniques. 5. **Proofs of Program Correctness**: The most important property of a program is its correctness. The paper argues that proving program correctness can reduce the costs associated with programming errors and improve reliability, documentation, and compatibility. 6. **Formal Language Definition**: The paper discusses the use of axioms for defining the semantics of high-level programming languages, ensuring compatibility among different implementations and facilitating better language design. The author concludes that while program proving is currently challenging, it offers significant theoretical and practical advantages, particularly in reducing errors and improving reliability.