Instead of first digging into the author's "Definition #3" and "Level 3 Design/Logic", I would recommend reading the 1985 paper "The Limits of Correctness" by Bryan Cantwell Smith.[1]

I think it's one of the top 5 papers every programmer should read. It's a short and easy read that makes one think about the limits of models, the limits of specifications, and the limits of formal verification. After grokking BCS's insights, there seems to be (an unintended) hubris in James Koppel's statement, "I now have two years experience teaching engineers a better understanding of how to [...] make code future-proof" in his framework of removing defects from "Level 3" design.

(As a side note, there's also a cosmic irony as that paper starts with an anecdote about the "correctness" of detecting ballistic missiles in 1960 given the recent false alarm in Hawaii.)

[1] https://www.student.cs.uwaterloo.ca/~cs492/11public_html/p18...