4 ms·
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 compil
by xamuel 9y ago
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.
- saagarjha 9y agoWhich would be essentially impossible for any language like C.
- nickpsecurity 9y agoKCC 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 https://github.com/kframework/c-semantics http://fsl.cs.illinois.edu/pubs/ellison-rosu-2012-popl.pdf http://fsl.cs.illinois.edu/pubs/ellison-rosu-2012-popl.pdf