What is "Programming Logic?" (memo)

Programming logic is a framework or system to prove properties of programs. Hoare logic is the representative basic theory, and certified programming is the technique/method for the programming logic. Hence "Programming language" and "programming logic" are different in the sense that the latter is a framework for proving properties of program, but former is usually just a language to construct programs but does not give a framework to prove properties of programs.