In Coq, there are 2 types (Prop and Set), they are used by the programmer to separate what are proofs that won't produce actual code and the part of the proof that will be used to extract running code (your program).
That is a nice solution for the problem you ask about, how to identify what is meant to generate machine code (program) and what is present to complete the proof of the proposition (or type).
AFAIK there is no automatic way to distinguish both. This might be something interesting for research? Or maybe someone is able to point out it's clearly impossible?
With dependent types not only there isn't a clear distinction between proofs and programs but also there isn't a distinction between programs and types! The only distinction will be where the type(or program) appear, making it part of the "program" place or of the "type" place of a given term.
An example will make it clearer i hope:
When you use the identity function with dependent types you need to pass the type your are going to use the function with! The type is being used as a value in your "program"!
Untyped Lambda Calculus:
id = $\lambda{x}.x$
With Dependent Types:
id : (A : Set) -> A -> A
id = $(\lambda{A}.(\lambda{x}.x))$
If you are using this function, then you would do it like this example:
id Naturals 1
Notice that the "type" (in this case the Set of Naturals) being passed as a value is thrown away so it will never be computed, but still it's in the "program" part of the term. That's what also will happen with the "proof" parts, they need to be there for the term to type-check but during computation they will be thrown away.