Some examples from E

I had ten minutes before lunch, and decided to code up a couple of examples from E in Haskell:

type Cont a = a -> STM ()

-- Blocking caretaker - requests are blocked until the gate is open
-- Note that the gate can be opened/closed repeatedly.
makeCaretaker :: Cont a -> STM (Cont a, Cont Bool)
makeCaretaker target = do 
  enabled <- newTVar True
  return (\m -> do {e <- readTVar enabled ; if e then target m else retry}, writeTVar enabled)
  
-- Overwritable promise.
makePromise :: STM (Cont a, Cont (Cont a))
makePromise = do
  queue <- newTChan
  target <- newTVar Nothing
  return (\m -> do
    t <- readTVar target
    case t of
      Nothing -> writeTChan queue m
      Just r -> r m
    , writeTVar target . Just)

Note that both caretaker and promise allow the controller to change its mind - either by repeatedly opening/closing the gate, or by re-resolving the reference. Also, when closed, the caretaker does not signal errors or swallow messages - it keeps the senders blocked. OTOH, promise stores messages in a queue.
Of course, this can be changed (I leave this as an exercise for readers :-) ).
I may consider creating a small library of such patterns and see whether something DSLish comes of it...
But before that I must decide on verification procedure - should I use unit tests or proofs...