Hacker News
new
|
past
|
comments
|
ask
|
show
|
jobs
|
submit
login
xamuel
on March 23, 2018
|
parent
|
context
|
favorite
| on:
C for All
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
on March 23, 2018
[–]
Which would be essentially impossible for any language like C.
nickpsecurity
on March 24, 2018
|
parent
[–]
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: