The Curry-Howard correspondence is often brought up as a relation between proving and programming, but at least Martin-Löf actually attributes the connection to programming to Kolmogorov. Whereas today types are easily associated with programming, Martin-Löf presents the connection in the order Types-Proposition-Problems (whose "solutions" are programs), that's kinda surprising today. Read his seminal paper, Constructive mathematics and computer programming.
Welcome to your niu world ! We are a cute and loving international community Ｏ(≧▽≦)Ｏ !