This paper aims to provide a formal basis for defining the meanings of programs in appropriately defined programming languages, establishing a rigorous standard for proofs about computer programs, including correctness, equivalence, and termination. The approach is based on the notion of an interpretation of a program, where each connection in the flow of control is associated with a proposition that is asserted to hold when that connection is taken. A condition is imposed on each command to ensure that if a command is reached via a connection with a true proposition, it will be left via a connection with a true proposition. This allows for inductive proofs about programs, such as showing that if initial variable values satisfy a relation, final values will satisfy another relation. Termination proofs are achieved by showing that each step decreases some entity that cannot decrease indefinitely. These proof methods are not original but are based on ideas from Perlis and Gorn. The paper proposes formal standards for proofs about programs in languages that allow assignments and control transfer, and suggests that the semantics of a programming language can be defined independently of processors, by establishing rigorous proof standards. A semantic definition of a programming language is based on a syntactic definition, specifying which phrases represent commands and the conditions on interpretations near each command. The paper demonstrates these concepts using a flowchart language and fragments of ALGOL. A flowchart is loosely defined as a directed graph with commands at each vertex. An interpretation maps edges to propositions, with some free variables representing program variables. A verification of an interpretation is a proof that if control enters a command via an entrance with a true proposition, it must leave via an exit with a true proposition. A semantic definition of command types involves constructing verification conditions for antecedents and consequents of commands. If these conditions are satisfied, the interpreted flowchart is verified.This paper aims to provide a formal basis for defining the meanings of programs in appropriately defined programming languages, establishing a rigorous standard for proofs about computer programs, including correctness, equivalence, and termination. The approach is based on the notion of an interpretation of a program, where each connection in the flow of control is associated with a proposition that is asserted to hold when that connection is taken. A condition is imposed on each command to ensure that if a command is reached via a connection with a true proposition, it will be left via a connection with a true proposition. This allows for inductive proofs about programs, such as showing that if initial variable values satisfy a relation, final values will satisfy another relation. Termination proofs are achieved by showing that each step decreases some entity that cannot decrease indefinitely. These proof methods are not original but are based on ideas from Perlis and Gorn. The paper proposes formal standards for proofs about programs in languages that allow assignments and control transfer, and suggests that the semantics of a programming language can be defined independently of processors, by establishing rigorous proof standards. A semantic definition of a programming language is based on a syntactic definition, specifying which phrases represent commands and the conditions on interpretations near each command. The paper demonstrates these concepts using a flowchart language and fragments of ALGOL. A flowchart is loosely defined as a directed graph with commands at each vertex. An interpretation maps edges to propositions, with some free variables representing program variables. A verification of an interpretation is a proof that if control enters a command via an entrance with a true proposition, it must leave via an exit with a true proposition. A semantic definition of command types involves constructing verification conditions for antecedents and consequents of commands. If these conditions are satisfied, the interpreted flowchart is verified.