As someone who teaches PL theory and has worked in PL theory for many years now, I love the the formulae-as-types notion of construction, also known as the Curry-Howard correspondence. It demonstrates a profound connection between lambda calculi and logic. Wadler's paper and accompanying talk provide an approachable introduction to the topic.
Yet, among the audience for such talks (which are primarily geared at functional programming practitioners rather than academics) are many who, I think, are getting the wrong message somehow. I see muddled, severely distorted, or even outright untrue claims being made about type theory and Curry-Howard quite frequently as a result of these misconceptions. So, to clear the air, I'll state my thesis up-front:
Learn it if you want, but it will not and cannot aid you in improving your programming practice (unless you're writing Idris or Lean!).
The Curry-Howard correspondence says that types correspond to propositions (or formulae) and programs that inhabit these types correspond to proofs of their respective propositions. So, programs are proofs, yes, but proofs about what?. Certainly not the programs themselves — without a dependently-typed language, we can't state propositions about programs on the type level. For most standard type systems, our propositions take the form of abstract logical sentences in a fairly limited (and inconsistent) propositional or second order logic, not theorems about programs.
Far more problematic, though, is the culture of mathematical fetishism within the functional programming community: the use of mathematical jargon to obscure rather than clarify — to show superiority over others, rather than establishing a common vocabulary. One example of this is those who insist on calling the Curry-Howard correspondence "the Curry-Howard isomorphism" because it uses an exclusively mathematical term, "isomorphism", rather than the more commonly-used (and more accurate) "correspondence". They will often talk very confidently, using large amounts of mathematical jargon, where in reality the idea under discussion is either significantly more straightforward than indicated, or outright wrong. People who behave in this way are really toxic for a programming community. The only solution I can recommend is to try hard to exclude this kind of toxic behaviour from programming communities, and to devote resources to supporting those learners who would otherwise potentially be led astray by this kind of behaviour.