Best way to introduce Curry-Howard isomorphism I want to give a small talk about the Curry-Howard isomorphism to people who are not familiar with intuitionistic logic.  Personally, I think about intuitionistic logic just in the propositions-as-types manner, but if I introduce it that way, the isomorphism will appear pretty dull.
So, what I want to ask, is there an equally nice (introductory) approach to intuitionistic (propositional) logic, that has as little as possible to do with types, so that the isomorphism feels at least a little bit surprising?
EDIT: I came up with this idea, unsure where it will take me.
 A: I think that there are two ways to do it. The first is you could explain a derivation in proof-theoretic terms. Then you'd notice that when you "embed" the derivation as a proof term you get something that looks like a programming language. You could conclude with evaluation coming from Gentzen's inversion principle.
This is a little dull in my opinion because really we've just set things up so what we're saying is "obviously true". The result we end up with is kind of that an inductively defined system looks a lot like another inductively defined system. The real weight behind this approach is that it's a useful way of investigating new areas of proof theory/computer science by drawing analogies to what is well known in other areas.
A somewhat more surprising interpretation of the props-as-types idea comes from Kleene. In his attempt to understand what was going on with constructive logic he came up with a realizability model. He took lambda calculus programs (actually horrible Godel numbered thing, please use LC) and showed that they could be used to model the "computation content" of a proof of some intuitionistic proposition.
This is much cooler in my mind because it gives a very concrete meaning to "proofs are programs". You can prove that a proposition which has a  proof has a program which computes according to its specification. So we'd say that a program realizes some proposition ($e \vDash A$) and if $A\ \text{true}$ holds then $\exists e.\ e \vDash A$. You'd define the relation $e \vDash A$ by induction on $A$. For example, if we suppose that we've Church encoded pairs, $e \vDash A \wedge B$ if $\pi_1 e \vDash A$ and $\pi_2 e \vDash B$ and similarly. This is a lot like the above but here the notion of computation is primitive to the set of things we're using to realize proofs, it's not something we define after the fact and the computation which occurs in these terms may be much richer than what we could derive from inversion principles.
I may be doing a poor job of explaining this but hopefully that makes some sense.
