[Ygg2]

Except in C, validation of user input can in itself be an exploit vector.

[layer8]

That’s true in other languages as well. Any programmatic task can end up being an exploit vector.

[pjc50]

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.

[rocketrascal]

You can fail to verify something which you actually wanted to verify (i.e you made a proof of something else instead of the thing that mattered). See WPA2 KRACK as an example.

[Ygg2]

Yeah, but only in C* can those errors end up as more UB.

* terms and limits may apply.

[eru]

Many other languages also have UB. But almost none is as trigger happy as C and C++ are.

[greybeard69]

Turtles all the way down.