Racket: contract-based programming
Developing a cryptographic solution means that the algorithm correctness is not an option. Not just for the hardware, firmware and application software, but also for manufacturing support software. Read on to see how we address this need.
Industrial software for controlling robots, for running CNC machines[1], or for verifying finished products against specification, demands the programmer is keen on putting as many defenses against run-time errors as possible. Once the software is deployed, any malfunction costs money. And very real money.
Writing correct[2] programs is not an easy task. However, before you try to do that, you should learn how to write correct components of some smaller type. For example individual functions[3] accepting some well-defined input and producing some output according to given specification. What does it mean – “well-defined input”?
Most people who did some programming (hopefully) heard of data types[4]. So the well-defined input might be a set of accepted data with data types. But how do we specify the data type? How and when can we check the value if it fits?
The list of questions can grow pretty quickly if we dive into the typing disciplines[5] of various programming languages. There are strictly static type systems where you must specify the variable type before you even assign the initial value to it or – on the other side of the spectrum – there are languages where you can mix anything with everything and vice-versa.
In Racket we have a dynamic – yet strong – typing discipline. You can pass values around as you like and you do not need to worry what type the value is. When you want to perform some operation that requires given data type, it will fail if you fail to provide it with the right arguments of the right types.
Consider the following simple example of number addition:
> (define a 1) > (define b 2) > (+ a b) 3
Now what if we try a string instead?
> (define a 1) > (define b "2") > (+ a b) ; +: contract violation ; expected: number? ; given: "2" ; argument position: 2nd ; [,bt for context]
Looks like the + function knows that it cannot work with strings and reports this to us. I also states that it expected “number?”. What is this? It is a predicate[6] and you can use it to test whether a given value is of given type:
> (number? a) #t > (number? b) #f > (string? a) #f > (string? b) #t
So without any further knowledge, you can easily ensure your functions always check if the arguments passed to them are valid and raise an error if the check fails. But that isn’t very elegant, is it?
Of course, Racket has its way of ensuring only the right data types get in and the right data types are produced as output. In Racket, contracts[7] are used for describing (and enforcing) that the expected input is given to a function and that output matches the specification.
Now to illustrate the concept, we will use a function that sums two elements of given list and returns the result:
(define (list-sum lst a b)
(+ (list-ref lst a)
(list-ref lst b)))
Just to show that it works:
> (list-sum (list 1 2 3) 0 2) 4
But what happens if we try something bad?
> (list-sum "1 2 3" 0 2) ; list-ref: contract violation ; expected: pair? ; given: "1 2 3" ; argument position: 1st ; [,bt for context] > (list-sum (list 1 2 3) 'x #f) ; list-ref: contract violation ; expected: exact-nonnegative-integer? ; given: 'x ; argument position: 2nd ; [,bt for context]
In the first example, no list is provided – rather a string is given. And in the second one, symbol and boolean values for the indices. Imagine for a moment we do not know the implementation of list-sum function and now we only see that an error happened calling list-ref function. Why list-ref when we are calling list-sum? Of course we know why and this is just a silly example. But even for such simple function, it should behave better from the perspective of its user. We can define a contract of what the function expects and what it produces:
(define/contract (list-sum lst a b)
(-> list? number? number? number?)
(+ (list-ref lst a)
(list-ref lst b)))
If such function is called with incorrect argument, more appropriate error is raised:
> (list-sum (list 1 2 3) 'x #f) ; list-sum: contract violation ; expected: number? ; given: 'x ; in: the 2nd argument of ; (-> (listof any/c) number? number? number?) ; contract from: (function list-sum) ; blaming: top-level ; (assuming the contract is correct) ; at: readline-input:20.18 ; [,bt for context]
If you think about this, you probably quickly come to a conclusion that no function should be left without a contract. And I can only second that conclusion. Of course, contract provide much more fin-grained means of checking the arguments and specifying the results – and we are using those heavily. But this was meant as and short introduction into the basic concepts of function contracts and how they can be used for ensuring that the basic building blocks of your programs are correct – that means they conform to their specification. If your specification is wrong, we get completely different story though.
Thanks for staying with us and be sure you get your Cryptoucan™ in 2020!
References
1. Wikipedia contributors. (2019, December 18). Numerical control. In Wikipedia, The Free Encyclopedia. Retrieved 22:04, January 1, 2020, from https://en.wikipedia.org/w/index.php?title=Numerical_control&oldid=931282710
2. Wikipedia contributors. (2020, January 1). Algorithm. In Wikipedia, The Free Encyclopedia. Retrieved 22:07, January 1, 2020, from https://en.wikipedia.org/w/index.php?title=Algorithm&oldid=933565576
3. Wikipedia contributors. (2019, December 31). Software. In Wikipedia, The Free Encyclopedia. Retrieved 22:08, January 1, 2020, from https://en.wikipedia.org/w/index.php?title=Software&oldid=933334444
4. Wikipedia contributors. (2019, December 8). Data type. In Wikipedia, The Free Encyclopedia. Retrieved 22:08, January 1, 2020, from https://en.wikipedia.org/w/index.php?title=Data_type&oldid=929748791
5. Wikipedia contributors. (2019, December 31). Type system. In Wikipedia, The Free Encyclopedia. Retrieved 22:08, January 1, 2020, from https://en.wikipedia.org/w/index.php?title=Type_system&oldid=933396080