[larve]

I would say it's the other way around:

1. Because the underlying concept for handling composing locks (STM, which I don't know much about, but I'm going to assume is a way to wrap operations within a transaction) is sound

2. it is easy to define the corresponding monad

3. which makes it usable in a do notation

4. producing readable and future-proof code

The step 2 is almost trivial, 1 is where the thinking is at. The do notation is nice to have, but not that important (to me at least). I have no problem writing this in CPS style when using javascript or c++:

   const transfer = (x, from, to, onSuccess, onError) => {
      return getAccountMoney(from, (f) => {
         if (f < x) { 
             return onError();
         } else { 
             return getAccountMoney(to, (t) => {
                 return setAccountMoney(to, t+x, () => {
                     return setAccountMoney(from, f-x, onSuccess, onError);
                 }, onError);
             }, onError);
         }, onError);
     }
   }

The main point is that I can add 80 edge cases to this and it will continue to compose nicely, not a single lock in sight.