Exactly! A very nice explanation of what is and what is not a proof by contradiction is given by R. Harper in "Proofs by contradiction, versus contradiction proofs" [1]
It is always a pleasure to read Daniel Jackson [1].
In this paper, Daniel revisits the ideas developed in his book, "The essence of software" [2].
placing them in their historical context and opening a future for more modular software implementations.
He presents a convincing argumentation on how and why an object-oriented approach does not really contribute to reducing coupling.
And his proposal is truly appealing: building an application as a set of external synchronization rules governing the interactions between modules (so called concepts). Each module comes with its own view on the entities of the application domain and provides the actions featuring the concept. Only the synchronization rules of the application relate the entities and actions of these modules.
That said, I'm left wanting more and I will need to take the time to put these ideas in code.
A proper doc definitely has to provide the details. However starting with an example or two is a nice way to a give the users a quick overview. Even better when this example is interactive as for redis where you even have an example use case. See https://redis.io/docs/latest/commands/incr/
Before any proof, the debate would benefit from more precise definitions.
For instance, the issue around the usage of fencing tokens to reject any late usage of a lock
is unclear just because the protected resource and its access are themselves unspecified.
Is the resource distributed or not?
If distributed, does the resource has a mean to ensure that tokens are increasing over all the nodes?
Does the resource have a mean to rollback any effects done by a client which session is interrupted by a timeout?
Likewise for the timing arguments.
It seems clear to everyone that timeouts provide only some protection rather than a guarantee.
A more precise timeline of the worst case scenario will help to estimate that protection given the misc timeout values and clock shifts.