Personal anecdote, inspired by something in social media:
In September 1975 I was a postgrad student at the University of Newcastle-on-Tyne, doing research on operating system command languages for my (never-completed) PhD. I was tapped as one of the three rapporteurs for a multi-day seminar on “programme correctness proof” with Djikstra. The format was simple; we’d take a fairly simple programme (probably something from volume 1 of Knuth) and collectively develop a proof of its correctness, led by Djikstra. Everybody in the Department was involved.
For those unfamiliar with the idea, “proof” generally refers to “Formal Verification”. The Wikipedia article captures the key idea:
The verification of these systems is done by ensuring the existence of a formal proof of a mathematical model of the system.
As this implies, the biggest challenge is actually developing the mathematical model for the program, a process that tends to be highly domain-specific. The number of rat-holes we explored was truly epic. I’m pretty sure we never actually completed the model, let alone the formal proof. And writing it all up was a nightmare….
I believe there’s a trip report about this in the ACM Library, but I don’t have the right level of access. It’s mentioned on this page.