The use of Predicate Calculus in coming up with the Proof along with the Program.

Predicate Calculus is used to show that the path followed by a Process through a Cartesian Product space (created from all the memory variables in a Program) is the one you had in mind w.r.t. its Specifications. Suddenly you start to understand basic Set Theory, Types, Relations (Functions) and Logic.