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

On that note: what even is a correct translation of C when it has so many undefined behaviors in it's spec.


They use a formally-specified subset of C described in Harvey Tuch's PhD thesis: http://www.ssrg.nicta.com.au/publications/papers/Tuch:phd.pd...


What if the code doesn't rely on undefined behavior?


Absence of undefined behavior in the C implementation is of course one of the things covered by the seL4 proof.




Consider applying for YC's Fall 2026 batch! Applications are open till July 27.

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

Search: