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

The only way to make C safe without losing performance would be to accompany your C code with a formal proof that it avoids undefined behavior, and use a compiler which refuses to compile the code if the formal proof doesn't validate.


Which would be essentially impossible for any language like C.


KCC is an executable, formal semantics for C that does something like that. Runtime Verification Inc uses it for their bug-hunting tools.

https://github.com/kframework/c-semantics

http://fsl.cs.illinois.edu/pubs/ellison-rosu-2012-popl.pdf




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

Search: