I'm not sure which first step you are talking about. Typically, one would write ...

		cccbbbaaa on May 15, 2024 \| parent \| context \| favorite \| on: Translation of Rust's core and alloc crates to Coq... 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.