Yes. Floyd-Hoare logic is worth learning about in this sense — a formal system for imperative languages where the rules essentially say "given preconditions X a

Yes. Floyd-Hoare logic is worth learning about in this sense — a formal system for imperative languages where the rules essentially say "given preconditions X and code Y, if X is true before you run Y, we guarantee Z to be true afterwards". I've never ever ever proven code correct using this formalism, but that way of thinking permeates my every action as a programmer.