Curry Howard Correspondence

Came across this which is a link between computer programs and logic, in the sense that using computer programs to "prove" things is legit. My interpretation of this is that it shows that constructs we use in computers languages can solve the same problems we solve using logic --

https://www.quora.com/Why-is-the-Curry-Howard-isomorphism-interesting

Not really a big deal, but something to make a note of, for future reference.