Yes. But it's a rare programmer, or even a programming language designer, who thinks of well-typed programs in terms of proving theorems.

They are. I avoided introducing an explanation of Curry-Howard isomorphism because I think that would not be very intuitive to many people because the most commonly used type systems have very little power to express logical properties about the program.

I may write another article about this.