This paper presents an axiomatic approach to computer programming, drawing on techniques used in geometry and mathematics. It explores the logical foundations of programming by defining sets of axioms and rules of inference for proving program properties. Examples of such axioms and rules are given, and a formal proof of a simple theorem is demonstrated. The paper argues that pursuing these topics offers both theoretical and practical advantages. Computer arithmetic is discussed, noting that while it differs from traditional mathematics, certain axioms can still be applied. The paper illustrates how different overflow handling techniques (strict, firm boundary, modulo arithmetic) can be distinguished by supplementary axioms. These axioms allow for the deduction of program properties, though the results depend on the implementation satisfying the chosen axioms. Program execution is analyzed, focusing on the correctness of programs. The paper introduces a notation for expressing the relationship between preconditions, programs, and postconditions. It discusses several rules of inference, including the axiom of assignment, rules of consequence, composition, iteration, and their applications in proving program correctness. An example is given of a program that computes the quotient and remainder of division, with a formal proof of its correctness. The paper emphasizes the importance of formal proofs in ensuring program correctness, though they can be tedious. It suggests that general rules for proof construction can reduce this tedium. The paper also addresses limitations of the axiomatic approach, such as the inability to prove program termination and the need to account for side effects. It notes that the axiomatic method can be extended to define programming languages, providing a formal basis for language semantics and aiding in the design of better languages. The paper concludes that program proving is not only a theoretical pursuit but also a practical one, offering benefits in reducing programming errors and improving software reliability, documentation, and compatibility. It acknowledges the challenges of applying this approach to complex programs but argues that the benefits outweigh the difficulties. The axiomatic method is seen as a valuable tool for defining programming languages and ensuring their correctness.This paper presents an axiomatic approach to computer programming, drawing on techniques used in geometry and mathematics. It explores the logical foundations of programming by defining sets of axioms and rules of inference for proving program properties. Examples of such axioms and rules are given, and a formal proof of a simple theorem is demonstrated. The paper argues that pursuing these topics offers both theoretical and practical advantages. Computer arithmetic is discussed, noting that while it differs from traditional mathematics, certain axioms can still be applied. The paper illustrates how different overflow handling techniques (strict, firm boundary, modulo arithmetic) can be distinguished by supplementary axioms. These axioms allow for the deduction of program properties, though the results depend on the implementation satisfying the chosen axioms. Program execution is analyzed, focusing on the correctness of programs. The paper introduces a notation for expressing the relationship between preconditions, programs, and postconditions. It discusses several rules of inference, including the axiom of assignment, rules of consequence, composition, iteration, and their applications in proving program correctness. An example is given of a program that computes the quotient and remainder of division, with a formal proof of its correctness. The paper emphasizes the importance of formal proofs in ensuring program correctness, though they can be tedious. It suggests that general rules for proof construction can reduce this tedium. The paper also addresses limitations of the axiomatic approach, such as the inability to prove program termination and the need to account for side effects. It notes that the axiomatic method can be extended to define programming languages, providing a formal basis for language semantics and aiding in the design of better languages. The paper concludes that program proving is not only a theoretical pursuit but also a practical one, offering benefits in reducing programming errors and improving software reliability, documentation, and compatibility. It acknowledges the challenges of applying this approach to complex programs but argues that the benefits outweigh the difficulties. The axiomatic method is seen as a valuable tool for defining programming languages and ensuring their correctness.