I'm not sure which first step you are talking about. Typically, one would write the program directly in Coq and use the extracted code as-is.