Given the “programs as proofs” isomorphism, how do we know that the program isn't lying?

Question

I've been studying constructive type theory (CTT) and one of the things that I'm not clear on is the proof part: Proving the correctness of a program in a form of a proof that's nothing but the program itself (Curry-Howard Correspondence)

Most examples that I've seen in books (e.g., Type Theory and Functional Programming - Thomson and TaPL) show the "proofs" on $\lambda$-abstractions and applications on terms (i.e., literally $a, b, e...$). The proofs seem to mostly rely on the type signatures of the functions, under the assumption that the function does what it claims. Not much is discussed about the "how" of the function's correctness.

For example, when writing a real program (e.g., in Haskell and other [pure] functional languages), the function under consideration could do any arbitrary computation and return a term of the correct type for the proof to go through (statically speaking). 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?

From what I understand, here's how things should go (and probably are, but I'm not sure if I'm right), crudely speaking:

1. Given a program's specification in something like predicate logic we "convert" it into an equivalent "typed representation"
2. Using backward inference we substitute the "functions" with their appropriate values, which themselves could be other functions (i.e., we replace the functions with their computation rules, but I'm thinking more on the lines of replacing the function with its body, from a programming point of view, for the sake of argument. Assuming that they're "returning" the correct type this seems like a believable substitution)
3. We continue doing #2 above till we hit primitive operations (again, crudely speaking) which we can trivially prove (or if not, maybe the proof is "simple" enough).
4. Once we've hit all the "axioms" (or trivial proofs) along all the branches of backward inferences, we stop.
5. QED

Two questions:

• Is my understanding/intuition of "how" the proof of correctness works in CTT works correct? It looks like it won't be possible for the program to "cheat" this or can it?
• And secondly, is this what proof assistants like Coq help you prove/analyze (at a high level)?