Ideal software is correct; that is, it does what it’s required to do and nothing else.

There are basically two routes to this ideal:

1. Write the software in such a way that it can be proven to be correct before it’s deployed in production
2. Converge to the ideal progressively by fixing bugs in production

The first route is usually taken in safety-critical applications like FinTech, where the cost of bugs in production outweighs higher development costs. The latter are driven up by the need to use non-mainstream technologies and also by higher overall complexity of the development process which, usually, comprises three main phases:

1. Rewriting customer’s requirements in a formal language (e.g. SPARK contracts)
2. Implementing the software in a programming language (e.g. SPARK)
3. Checking the implementation against the formal requirements, using a theorem prover (e.g. GNATprove)

In most cases, however, the cost of bugs in production doesn’t justify the investment in a provably correct software; consequently, the users must tolerate a certain amount of bugs because their ranting just doesn’t hurt as much as paying for bug-free software. We hear them; in this post, I’ll show you how Clojure makes it possible to write cheap but correct software. More precisely, since Clojure is such a high-level language, it can serve both as a language for formalizing the requirements and as a language for implementing them, effectively squashing the three phases above into one.

Programming as a reduction of a list of requirements

We’ll approach the problem of writing correct software similarly to how Clojure approaches that of adding a list of five numbers:

(reduce + [1 2 3 4 5])

which essentially expands to:

(+ 5 (+ 4 (+ 3 (+ 2 (+ 1 (reduce + [])))))

where

(reduce + [])

is defined to be zero. Clearly, the following two invariants hold:

1. After the zero-th step of the computation ((reduce + [])), we’re left with the sum of the first 0 numbers (since (reduce + []) is defined to be 0, the sum of the first 0 numbers).
2. If what we got from the n-th step of the computation is the sum of the first n numbers, then the output of the (n + 1)-th step of the computation will be the (n + 1)-th number plus the sum of the first n numbers (see the computation above), that is, the sum of the first (n + 1) numbers.

By induction, it follows that after the 5th step of the computation, we’re left with the sum of the first 5 numbers, which is the same as the sum of the entire list. Now, imagine that we replace the list of numbers with a list of requirements and the + operator with another binary “operator” which, given implementation and a requirement, extends the implementation in such a way that it

1. satisfies the requirement 
2. doesn’t interfere with the already satisfied requirements

Then, by induction, after processing the complete list of requirements, we are left with an implementation that satisfies all the requirements. Of course, the difficult part is ensuring, after each step, that the implementation satisfies the just processed requirement and that the just processed requirement doesn’t interfere with the requirements processed earlier. In the following section, we’ll see how Clojure helps us tremendously with this difficult task.

ClojureCoin

Imagine a customer comes to us with the following requirements:

We want a virtual coin that users can send to other users. Our requirements are:

1. A user can only send a number of coins which is a positive integer
2. A user can only send an amount if his/her balance is sufficient
3. Transactions with payee identical to payer will be disallowed

In case any of the conditions above are not met, an informative error will be thrown. Moreover, 

4. If an amount of coins is sent, it must be sent to the payee specified in the transaction. 

Last but not least,

5. It must be impossible to send the same coin to a user at the same time as it was sent to another user and immediately after that.

The first four conditions above are pretty straightforward and we could just sit down and write the code straight away. However, the last requirement, the so-called “impossibility of double spending”, is trickier and needs some “refinement”. We can draw some inspiration from the original Bitcoin paper by Satoshi Nakamoto (page 2):

“We define an electronic coin as a chain of digital signatures.”

Indeed, the following two conditions make sending a coin to two different users in direct succession impossible:

1. sending a coin is equivalent to changing its owner
2. a coin can only be spent by its owner

Assume a coin has been sent to a user and immediately sent to a different user. Then, by (a), its owner changed as a result of the first transaction. By (b), it can no longer be sent by its original owner after the first transaction, which contradicts our assumption that a second transaction with the same coin followed. To address the second scenario, that of a user sending the same coin to multiple users at the same time, we only need to make sure that

3. at any given time, a coin can only have a single owner

Indeed, assume that a user sends the same coin to two different users at the same time. Then, by (a), its owner has changed to two different owners at the same time, which contradicts (c). Even if a coin can’t be sent to two different users at the same time, running the two transactions in parallel could potentially result in the coin being in an inconsistent state; that is, instead of being sent to user A and user B, it could be sent to a “crossover” user AB, contradicting (4) above. Hence, we introduce one more requirement:

4. running two transactions in parallel never results in an inconsistent state of any of the affected coins

Finally, we are left with the following list of requirements to reduce:

1. A user can only send a number of coins which is a positive integer
2. A user can only send an amount if his/her balance is sufficient
3. Transactions with payee identical to payer will be disallowed
4. If an amount of coins is sent, it must be sent to the payee specified in the transaction.

1. sending a coin is equivalent to changing its owner
2. a coin can only be spent by its owner
3. at any given time, a coin can only have a single owner
4. running two transactions in parallel never results in an inconsistent state of any of the affected coins

Our initial implementation, to be extended to satisfy the requirements above, looks like this:

(defn dispatch
[arg]
(-> arg keys set))
(defmulti get-payer-balance dispatch)
(defmulti validate dispatch)
(defmulti send! dispatch)
(defmethod send! #{:coins :transaction/amount :transaction/payer :transaction/payee}
[arg]
(dosync (-> arg get-payer-balance validate send!)))

The send! function will be called by a payer in order to send a certain amount from the shared pool of coins to a payee. One might ask why we use multimethods here, as there is apparently no need for polymorphism. There are two main reasons: first, a need for polymorphism might arise in the future; for instance, as an alternative to passing :coins, :transaction/amount, :transaction/payer, and :transaction/payee to the send! method above, we might want to pass :database/connection and :transaction/id to it, pulling the necessary data from a database. Second, Clojure multimethods provide a succinct way to express invariants which hold when a given method is called during program execution; for instance, by definition of the dispatch function above, when the send! method is called, we can be sure the arg map contains the fields listed above; if it didn’t, the method wouldn’t have been called, as guaranteed by the multimethod machinery.

The first requirement to extend the initial implementation will be:

c. at any given time, a coin can only have a single owner

The code snippet to address the requirement is:

(defmulti owner dispatch)
(defmethod owner #{:coin}
[arg]
(deref (:coin arg)))

deref is a Clojure function for retrieving a value of a reference; since each Clojure reference only has a single value at a given time, the requirement is satisfied. As this is the first requirement to be addressed, there are no earlier requirements to check for interference and hence we can proceed to the second requirement:

d. running two transactions in parallel never results in an inconsistent state of any of the affected coins

This one can be handled by:

(defmulti change-owner! dispatch)
(defmethod change-owner! #{:coin :valid-transaction/payee}
[arg]
(ref-set (:coin arg) (:valid-transaction/payee arg)))

As per the implementation of Clojure, ref-set is guaranteed to never result in an inconsistent state of the reference being set. Also, “splitting” the reference so that it would suddenly have multiple values is impossible and hence the previous requirement is not affected. Next requirement:

b. a coin can only be spent by its owner

Code snippet:

(defmethod get-payer-balance #{:coins :transaction/amount :transaction/payer :transaction/payee}
[arg]
{:payer-balance      (filter #(= (owner {:coin %}) (:transaction/payer arg)) (:coins arg))
  :transaction/amount (:transaction/amount arg)
  :transaction/payer  (:transaction/payer arg)
  :transaction/payee  (:transaction/payee arg)})

Note that our system is essentially a pipeline:

(defmethod send! #{:coins :transaction/amount :transaction/payer :transaction/payee}
[arg]
(dosync (-> arg get-payer-balance validate send!)))

What we send down the pipe are just the coins that belong to the payer specified in the transaction (payer balance) and hence the requirement is satisfied. As this code snippet doesn’t affect the implementation of the owner and change-owner! methods, the earlier two requirements are unaffected, too, and we can proceed to the next requirement. This time, we’ll handle three requirements with one code snippet:

1. A user can only send a number of coins which is a positive integer
2. A user can only send an amount if his/her balance is sufficient
3. Transactions with payee identical to payer will be disallowed

In case any of the conditions above are not met, an informative error will be thrown.

The code snippet:

(defmethod validate #{:payer-balance :transaction/amount :transaction/payer :transaction/payee}
[arg]
(when-not (pos-int? (:transaction/amount arg))
  (throw (Exception. "Invalid amount!")))
(when (> (:transaction/amount arg) (count (:payer-balance arg)))
  (throw (Exception. "Insufficient balance!")))
(when (= (:transaction/payee arg) (:transaction/payer arg))
  (throw (Exception. "Payee must differ from payer!")))
{:payer-balance            (:payer-balance arg)
  :valid-transaction/amount (:transaction/amount arg)
  :valid-transaction/payee  (:transaction/payee arg)})

The code is pretty straightforward, we only need to make sure that the validation is performed before any coins are sent and we validate the transaction against a correct balance. Looking at our pipeline once again:

(defmethod send! #{:coins :transaction/amount :transaction/payer :transaction/payee}
[arg]
(dosync (-> arg get-payer-balance validate send!)))

we see that the validation indeed precedes any sending of coins. Further, since the previous code snippet:

(defmethod get-payer-balance #{:coins :transaction/amount :transaction/payer :transaction/payee}
[arg]
{:payer-balance      (filter #(= (owner {:coin %}) (:transaction/payer arg)) (:coins arg))
  :transaction/amount (:transaction/amount arg)
  :transaction/payer  (:transaction/payer arg)
  :transaction/payee  (:transaction/payee arg)})

filters the shared pool of coins based on the transaction and passes the transaction through, the validate method is guaranteed to be called with the correct balance. Hence, the requirement is satisfied and since we don’t fiddle with implementation of any of the methods defined earlier, we’re free to proceed to another requirement:

1. sending a coin is equivalent to changing its owner

The code snippet:

(defmethod send! #{:payer-balance :valid-transaction/amount :valid-transaction/payee}
[arg]
(->> (:payer-balance arg)
      (take (:valid-transaction/amount arg))
      (map #(change-owner! {:coin % :valid-transaction/payee (:valid-transaction/payee arg)}))
      doall))

As per our pipeline:

(defmethod send! #{:coins :transaction/amount :transaction/payer :transaction/payee}
[arg]
(dosync (-> arg get-payer-balance validate send!)))

and the previous code snippets, the method above will be called after the validation was performed; it follows that the payee is different from the payer. Recalling the definitions of the owner and change-owner! methods:

<!-- wp:preformatted -->
<pre class="wp-block-preformatted">(<strong>defmethod</strong> owner #{:coin}
[arg]
(<strong>deref</strong> (:coin arg)))</pre>
<!-- /wp:preformatted -->

<!-- wp:preformatted -->
<pre class="wp-block-preformatted">(<strong>defmethod</strong> change-owner! #{:coin :valid-transaction/payee}
[arg]
(<strong>ref-set</strong> (:coin arg) (:valid-transaction/payee arg)))</pre>
<!-- /wp:preformatted -->

it’s clear that all the coins to be sent will have their owner changed. However, note that at this final stage of the pipeline, we are changing the values on which the earlier steps depend. In a multithreaded context, it might very well happen that a coin is sent by one thread after its owner has been determined by another thread but before the coin has been sent by the latter thread. Fortunately, our entire pipeline is wrapped in a transaction (dosync):

(defmethod send! #{:coins :transaction/amount :transaction/payer :transaction/payee}
[arg]
(dosync (-> arg get-payer-balance validate send!)))

Whenever a coin should be sent by the latter thread which was sent by the former thread after its owner was determined by the latter thread, the entire transaction will be restarted in the latter thread.  Hence, no problem here and we can proceed to the last remaining requirement:

4. if an amount of coins is sent, it must be sent to the payee specified in the transaction.

This requirement has already been satisfied, no additional code is needed. Indeed, going through the entire pipeline, we see that the transaction is passed unchanged all the way to the final stage:

(defmethod send! #{:payer-balance :valid-transaction/amount :valid-transaction/payee}
[arg]
(->> (:payer-balance arg)
      (take (:valid-transaction/amount arg))
      (map #(change-owner! {:coin % :valid-transaction/payee (:valid-transaction/payee arg)}))
      doall))

where the amount of coins is taken from the payer’s balance and the payee passed to the change-owner! method. Now, the reduction of requirements is complete and we can enjoy the result; running the code below in REPL:

(let [money (concat (repeatedly 3 #(ref "Michal")) (repeatedly 3 #(ref "Hana")))]
(prn (map #(owner {:coin %}) money))
(send! {:coins money :transaction/amount 1 :transaction/payer "Michal" :transaction/payee "Hana"})
(prn (map #(owner {:coin %}) money)))

the following gets printed:

("Michal" "Michal" "Michal" "Eliška" "Eliška" "Eliška")
("Eliška" "Michal" "Michal" "Eliška" "Eliška" "Eliška")

Note how the first coin changed its owner. Testing of the error scenarios is left to the reader 😉

Conclusion

When trying to prove that implementing a given requirement doesn’t interfere with the already implemented requirements, we often rely on the fact that requirements pertaining to different methods (functions) cannot interfere. This is made possible by using immutable data structures that abound in Clojure; with immutable data structures, one function cannot change data on which another function depends internally, and hence the two are truly independent. Clojure came to the rescue even when reasoning about the global mutable state (the pool of coins); its reference types provided the necessary guarantees.

To conclude, Clojure is well-equipped to support the cost-effective development of reliable software.