I don't know any practical way ... to write executable
descriptions of real algorithms and formal behavioral proofs that they satisfy
correctness properties. This is one reason why, in more than 35 years of writ-
ing concurrent algorithms, I have found behavioral reasoning to be unreliable
for more complicated algorithms. I believe another reason to be that behav-
ioral proofs are inherently more complex than state-based ones for sufficiently
complex algorithms. This leads people to write less rigorous behavioral proofs
for those algorithms, especially with no completely formal proofs to serve as
guideposts.
State-based reasoning also gives me confidence that concurrency is actually intuitively understandable. I my 30+ years of (successfully) working with distributed and concurrent software, we always felt queasy about it -- most people called it black art, believed that solid grasp was just beyond hope, that there wasn't a good way to enumerate all the possible time-interleavings of events. We felt lucky when it worked and ignorant when it didn't.