My practitioner view of program analysis

About ten years ago, I started thinking in earnest about how we could make it easier to write correct programs. Researching this question led me to topics like formal methods and type systems, techniques to help establish that a given program adheres to some rules. However, I was still unsure of how to prove that software was actually correct. Not in the sense that the executed instructions produce a result consistent with the specification, but in the sense that this program actually does what.