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

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.

Turtles all the way down.