|
| ▲ | layer8 3 hours ago | parent | next [-] |
| That’s true in other languages as well. Any programmatic task can end up being an exploit vector. |
| |
| ▲ | pjc50 2 hours ago | parent [-] | | 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. |
|
|
| ▲ | greybeard69 3 hours ago | parent | prev [-] |
| Turtles all the way down. |