Hacker News
new
|
past
|
comments
|
ask
|
show
|
jobs
|
submit
login
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.
Consider applying for YC's Summer 2026 batch! Applications are open till May 4
Guidelines
|
FAQ
|
Lists
|
API
|
Security
|
Legal
|
Apply to YC
|
Contact
Search:
My question was whether it can help detecting translation errors from the first step.