Does proofs are programs apply to any functional program?
In Haskell there are more programs than there are Coq proofs because Haskell has general recursion whereas Coq does not. (In fact Coq allows you to extract proofs into Haskell code.)

The reason that Coq does not have general recursion is that with it we can "prove" anything, simply by saying "to prove $t$ just make a recursive call to itself":

proveAnything :: t
proveAnything = proveAnything


In some languages, for instance in OCaml, you can't do it this way so you have to go indirectly through a recursive function call:

let rec proveAnythingAux _ = proveAnythingAux ()
let proveAnything = proveAnythingAux ()


This shows that type theory can be used for many things, two of which are programming and logic. The difference between these two is general recursion: we want it in programming but it makes logic inconsistent.