With proofs of correctness, I think it's important to recognize that systems will need to be built in a way that is conducive to proving statements about them. This is a practical daily endeavor for anyone who uses static type systems to catch errors (since types are theorems if you squint), and a major driving idea behind functional programming research. Compositionality and purity can make it drastically easier to prove interesting theorems about programs.