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

Have you seen CakeML[0]? It is verified that the semantics of the x86 machine code it outputs in the end are the same as the SML code it takes as input, up to out-of-memory errors.

[0]: https://cakeml.org/



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

Search: