To simplify shared-memory concurrent programming, in addition to low-level synchronisation primitives, several modern programming languages have started to offer core support for higher-level communication primitives as well, in the guise of message passing through channels. Yet, a growing body of evidence suggests that channel-based programming abstractions for shared memory also have their issues. The Discourje project aims to help programmers cope with message-passing concurrency bugs in Clojure programs, based on run-time verification and dynamic monitoring. The idea is that programmers write not only implementations, but also specifications (of sessions of channel actions). Discourje then offers a library to ensure that implementations run safely relative to specifications (= “bad” channel actions never happen). This paper gives a tour of the current state of Discourje, by example; it is intended to serve both as a general overview for readers who are unfamiliar with previous work on Discourje, and as an introduction to new features for readers who are familiar.
Lecture Notes in Computer Science
International Symposium on Leveraging Applications of Formal Methods
Centrum Wiskunde & Informatica, Amsterdam (CWI), The Netherlands

Hamers, R, & Jongmans, S.-S.T.Q. (2020). Safe sessions of channel actions in Clojure: A tour of the Discourje Project. In Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles (pp. 489–508). doi:10.1007/978-3-030-61362-4_28