alt Hacker NewsThat’s true in other languages as well. Any programmatic task can end up being an exploit vector.
Replies
Ygg2 • yesterday at 3:11 PM
Yeah, but only in C* can those errors end up as more UB.
* terms and limits may apply.
That’s true in other languages as well. Any programmatic task can end up being an exploit vector.
Yeah, but only in C* can those errors end up as more UB.
* terms and limits may apply.
No? That's the whole point of formal verification?
You can even kind of retrofit this to C. The classic example is "sel4". You just need a set of proofs that the code doesn't trigger UB. This ends up being much larger and more complicated than the C itself.