> Part of the linked paper's point is that because computer systems involve many "levels of failure", even a more careful programmer cannot usually rule out eve

> Part of the linked paper's point is that because computer systems involve many "levels of failure", even a more careful programmer cannot usually rule out every class of programs. The programmer only has to comply with the specification. The specification is a finite syntactic entity. If the specification doesn't capture what the user really wants, or compliance is undecidable, or <insert problem beyond the programmer's control here>, then the one at fault is the specification writer, not the programmer.