Constructing a formal proof is not only related to programming, it's the same thing. Curry–Howard correspondence:

"In programming language theory and proof theory, the Curry–Howard correspondence is a direct relationship between computer programs and mathematical proofs. It is also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation."

https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...