I laughed at formal methods of program proof until I came across a simplified version of cleanroom development methodology (which breaks program components into 'program primes' like A then B, If A then B, While A do B and for A in B do C) that allowed you to formally prove outcomes on paper. I have long since lost the document but to this day, I construct most of my work around these primes for certain projects.
That sounds a bit like Hoare logic [0], refinement calculus [1], or guarded command language [2]. The term "program prime" is not something I've heard or read before and I'm not turning up much.
Goodness knows why my original comment is being downvoted. The formal term is 'primary program refinement' and can be found all over the place such as here:
