Some references below. You'd probably want to start with the first 3. The other 3 are classics, but much more dense (e.g. the Nielsons book requires some decent abstract algebra background):

* Software Foundations (Pierce): https://softwarefoundations.cis.upenn.edu/

* Concrete Semantics (Nipkow): http://www21.in.tum.de/~nipkow/Concrete-Semantics/

* FRAP (Chlipala): http://adam.chlipala.net/frap/

* Model checking (Katoen): https://mitpress.mit.edu/books/principles-model-checking

* Program analysis & abstract interpretation (the Nielsons): https://www.springer.com/gb/book/9783540654100

* Type systems (Pierce): https://www.cis.upenn.edu/~bcpierce/tapl/

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.