Yes, I know, I mentioned the extraction. My question was whether it can help det... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		user2342 on May 15, 2024 \| parent \| context \| favorite \| on: Translation of Rust's core and alloc crates to Coq... Yes, I know, I mentioned the extraction. My question was whether it can help detecting translation errors from the first step.

cccbbbaaa on May 15, 2024 [–]

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.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact