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.