Given the "programs as proofs" isomorphism, how do we know that the program isn't lying?
Proving the correctness of a program in a form of a proof that's nothing but the program itself 


This is not quite how the Curry-Howard-Correspondence works.

First one has to show that the language of choice actually corresponds to some consistent logic. Different languages correspond to different logics, and many languages correspond to inconsistent logics which are not good for proving things. Haskell doesn't correspond to a consistent logic, because in Haskell, we can write nonterminating programs which would correspond to infinite proofs. But infinite proofs are invalid, so not every Haskell program corresponds to a valid proof.

Now what does it mean that a language corresponds to a logic? It means that:


a type in the language corresponds to a formula in the logic
a program in the language corresponds to a description of a proof in the logic
a well-typed program in the language corresponds to a description of a valid proof in the logic.
a program of a specific type in the language corresponds to a proof of a specific formula in the logic
a value in the language correspond to truth in the logic
evaluation of programs to values corresponds to soundness of the proving rules
reification of values to programs corresponds to completeness of the proving rules
...


No need to understand all aspects of the correspondence at once, but it is good to keep in mind that the correspondence relates not just programs and proofs, but many (all?) aspects of the languages and the logic. For the question here, only the first four aspects are relevant.

A minor issue is that only well-typed programs correspond to valid proofs. That's why type signatures of functions are so relevant to the Curry-Howard-Correspondence.

The key issue is that a well-typed program doesn't correspond to a valid proof of its own correctness, but to a valid proof of whatever formula corresponds to the program's type.

For example, let us consider the following two programs (using Haskell syntax, but assuming a version of Haskell that corresponds to a consistent logic):

f :: a -&gt; a -&gt; a
f x y = x

g :: a -&gt; a -&gt; a
g x y = y


The functions f and g are well-typed programs of the same type, so they correspond to valid proofs of the same formula. The formula is "forall propositions p, p implies that p implies p".

But clearly, f and g are different programs. And of course, they correspond to different proofs of the same formula. The program f corresponds to the proof "We know that p implies p, so also p implies (whatever implies p)". And the program g corresponds to the proof "We know that p implies p, so also whatever implies (p implies p)."

Usually, with programming languages, we care about the difference between programs like f and g, and with logics, we don't care about the difference between the two proofs that correspond to f and g. But when thinking about the Curry-Howard-Correspondence, it is important not to forget that there can be multiple different valid proofs of the same formula.


  So how do we know that the program is computationally doing the "right" thing (dynamically speaking) and not just faking it to get past a proofing system?


We don't. We only know that the program proves the formula we have encoded in the program's type. So how can we use the Curry-Howard-Correspondence to prove a program correct? We have to encode a statement about program correctness into the type of the program. This requires a very expressive type system, of course, which is exactly what the languages inside tools like Coq or Agda provide.