I read Dijkstra's goto considered harmful in college, circa 1970. I was a young programmer at the time, and it made me think and reconsider how and why big programs were often hard to understand.
Years later, in grad school, my research was on program verification. Dijkstra was a big influence on the field. I attended a lecture at UT Austin that he gave before moving to the US.
Dijkstra's approach to proving the correctness of programs is hard to apply in practice. Like a geometry proof, there are ways in which a proof of correctness can have mistakes that aren't obvious. Here's an example, prove that a sorting algorithm works. If the specification is that the output must be in sorted order, a proven program can still fail to sort correctly. The specification has an error, the output must not only be in sorted order, it must ensure that all of the input elements make it somewhere to the output. But this isn't good enough. A sort proven to meet this specification might leave out some duplicate values. Requiring that the output be the same length as the input still isn't good enough, multiple copies of one element might hide missing duplicate input values for another element. The specification requires that the output be a sorted permutation of the input.
Sorting is a well understood problem, but real verification must deal with the strange mathematics implemented by computers. The mathematical theories that we are accustomed to from school assume infinite precision and no overflow, real life hardware doesn't act this way.
All of this makes program verification hard, and my hope is that AI programming assistants will someday aid in the construction of meaningful specifications and work with the programmer to verify the correctness of programs or determine their safe operating boundaries. Progress has been slow, and the tools are still impractical for use by most programmers on most programs.
Program verification is a fool's errand and Dijkstra would have been the first to tell you this. The correct approach is program construction following derivation rules that do not admit error. You don't need to verify a program produced from a specification this way anymore than you need to prove a proof by construction. It baffles me that to this day the distinction defies comprehension for so many in our field.
Bugs can still occur of course, but if one restricts oneself to valid manipulations the bugs will be found in the specification and reflected in the code. It's not a magic bullet, and that's one of the reasons TLA+ was invented, it helps with complexity on the specification side. However a method like the one Dijkstra shows in the referenced paper can be used to faithfully implement the TLA+ checked specification.
Take a look at Frama-C or Ada Spark sometime; they apply the predicate transformer semantics style to code and do pretty well. But yeah, incomplete specifications are always fun.
This is such a great and actually important comment. I’ve been obsessed with program correctness / verification for a while now. It just seems like the holy grail that we can’t fully attain yet. But you keep bumping into certain walls, and the fact that correctness can only be relative to a given specification is a profoundly huge wall.
There’s no checking to see if your specification is under-specified.
Given what I've seen of AI today (works reasonably well at the best of times, but is sensitive to unusual cases and can produce totally nonsensical results otherwise; and nearly impossible to actually debug), I remain highly skeptical.
Within the context of theorem-proving, that's not as significant a problem -- you still have a verification of the proof at the end. The value of AI is that it could potentially replace human intuition for how to construct the proof. Humans don't always get this right either. It may take the AI many attempts to get the program right, but you'll know at the end that it is correct.
Years later, in grad school, my research was on program verification. Dijkstra was a big influence on the field. I attended a lecture at UT Austin that he gave before moving to the US.
Dijkstra's approach to proving the correctness of programs is hard to apply in practice. Like a geometry proof, there are ways in which a proof of correctness can have mistakes that aren't obvious. Here's an example, prove that a sorting algorithm works. If the specification is that the output must be in sorted order, a proven program can still fail to sort correctly. The specification has an error, the output must not only be in sorted order, it must ensure that all of the input elements make it somewhere to the output. But this isn't good enough. A sort proven to meet this specification might leave out some duplicate values. Requiring that the output be the same length as the input still isn't good enough, multiple copies of one element might hide missing duplicate input values for another element. The specification requires that the output be a sorted permutation of the input.
Sorting is a well understood problem, but real verification must deal with the strange mathematics implemented by computers. The mathematical theories that we are accustomed to from school assume infinite precision and no overflow, real life hardware doesn't act this way.
All of this makes program verification hard, and my hope is that AI programming assistants will someday aid in the construction of meaningful specifications and work with the programmer to verify the correctness of programs or determine their safe operating boundaries. Progress has been slow, and the tools are still impractical for use by most programmers on most programs.