[Sharlin]

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