This is a repost of a post in https://acm-fm-blog.blogspot.com/2020/04/formal-methods-usability-perspective.html
Welcome back to the ACM FM Blog. It has been a long time (5 months!) since I posted the first of what was to be a "series of posts" on usability of formal methods. I am afraid I have not lived up to my promise and initial enthusiasm. My excuse is that I am a novice when it comes to blogging and I was trying to "complete a post" -- and have been spectacularly unsuccessful. I have since come to the conclusion out that it is probably better to post something regularly and keep a dialog going rather than waiting for a "complete" post -- even at the cost of having to retract various statements and opinions and in general embarrassing myself. So, here goes!
I have been reading the classic book "The design of everyday things" by Don Norman; and would like to share some of my thoughts as I have been going through this book. As an aside, about the reading experience itself: I have been using a combination of Kindle and Audible to go through this book. I have found that listening to Audible while simultaneously reading on Kindle gives me a much more "immersive" experience. I am sure it would be better with a physical book (I can drop it, fold it backwards, scribble on it), but I do seem to enjoy the voice component quite a bit. I would encourage you to try it as well.
The book has a number of things that we can learn about in general, but my focus was really to try and relate it to formal-methods problems and solutions. Let me start with the very first "new" word I learnt from the book - "affordance". Now, I had not come across this word till I was working on product design at MathWorks; and the way MathWorkers were using it seemed to be a fancy way to talk about a graphical widget. The typical phrases I heard were: "what is the affordance for doing xyz", "is this affordance discoverable?" etc. (I have introduced another word "discoverable" that I will cover in a later post).
A Wikipedia search gave results that were not completely easy to understand and a some parts of the entry also referred back to this book! The explanation that I liked in the book is that an "affordance" is a "relation" between an object, the functions it can perform, and the operations that can be performed by a user on it to achieve these functions. A simple example is a chair that "affords" sitting. Trust me, his is not as trivial as it sounds! Most of us would have the image of a chair (from Wikipedia) like this. This is great and it is obvious that this chair "affords" sitting. But how about this chair, also from the same Wikipedia page? I am sure you will think twice before sitting on it. Another example is this chair -- I use a chair like this regularly, and I have seen so many people trying, unsuccessfully, to figure out how to sit in this chair (BTW, this is how you sit in this chair). Yet another interesting example is this -- I have still not figured out to use this chair without injuring myself!
Anyway, the point I want to make is that all the chairs in the last paragraph "afford" sitting. What they differ in how the design of the chair "signifies" the function it can perform to you (a user). A "signifier" is also a term introduced in the book as a mechanism for communicating an affordance which may otherwise not be perceived by the user. If an affordance is not perceived by a user, how can it be usable? Signifiers play an important role in the design of everyday things!
With the chairs, an interesting aspect to note is that "signifiers" are not completely context-free -- I am sure there are some of you for whom the way to use the different chairs is obvious: you have some background knowledge and are able to use the chair with no problems. This problem of "knowledge" is also addressed later in the book and I will not talk much about it now (another topic for a future post!)
Now let us apply this to formal methods and the work we are all involved in as a community. What are some examples of "affordances" and "signifiers" that we can associate with? The answers are not immediately obvious, but some examples I would like to briefly discuss are:
I hope this post directs you to think a little bit about affordances and signifiers. Do you have examples in your mind that you could share? I would love to hear your ideas.
Welcome back to the ACM FM Blog. It has been a long time (5 months!) since I posted the first of what was to be a "series of posts" on usability of formal methods. I am afraid I have not lived up to my promise and initial enthusiasm. My excuse is that I am a novice when it comes to blogging and I was trying to "complete a post" -- and have been spectacularly unsuccessful. I have since come to the conclusion out that it is probably better to post something regularly and keep a dialog going rather than waiting for a "complete" post -- even at the cost of having to retract various statements and opinions and in general embarrassing myself. So, here goes!
I have been reading the classic book "The design of everyday things" by Don Norman; and would like to share some of my thoughts as I have been going through this book. As an aside, about the reading experience itself: I have been using a combination of Kindle and Audible to go through this book. I have found that listening to Audible while simultaneously reading on Kindle gives me a much more "immersive" experience. I am sure it would be better with a physical book (I can drop it, fold it backwards, scribble on it), but I do seem to enjoy the voice component quite a bit. I would encourage you to try it as well.
The book has a number of things that we can learn about in general, but my focus was really to try and relate it to formal-methods problems and solutions. Let me start with the very first "new" word I learnt from the book - "affordance". Now, I had not come across this word till I was working on product design at MathWorks; and the way MathWorkers were using it seemed to be a fancy way to talk about a graphical widget. The typical phrases I heard were: "what is the affordance for doing xyz", "is this affordance discoverable?" etc. (I have introduced another word "discoverable" that I will cover in a later post).
A Wikipedia search gave results that were not completely easy to understand and a some parts of the entry also referred back to this book! The explanation that I liked in the book is that an "affordance" is a "relation" between an object, the functions it can perform, and the operations that can be performed by a user on it to achieve these functions. A simple example is a chair that "affords" sitting. Trust me, his is not as trivial as it sounds! Most of us would have the image of a chair (from Wikipedia) like this. This is great and it is obvious that this chair "affords" sitting. But how about this chair, also from the same Wikipedia page? I am sure you will think twice before sitting on it. Another example is this chair -- I use a chair like this regularly, and I have seen so many people trying, unsuccessfully, to figure out how to sit in this chair (BTW, this is how you sit in this chair). Yet another interesting example is this -- I have still not figured out to use this chair without injuring myself!
Anyway, the point I want to make is that all the chairs in the last paragraph "afford" sitting. What they differ in how the design of the chair "signifies" the function it can perform to you (a user). A "signifier" is also a term introduced in the book as a mechanism for communicating an affordance which may otherwise not be perceived by the user. If an affordance is not perceived by a user, how can it be usable? Signifiers play an important role in the design of everyday things!
With the chairs, an interesting aspect to note is that "signifiers" are not completely context-free -- I am sure there are some of you for whom the way to use the different chairs is obvious: you have some background knowledge and are able to use the chair with no problems. This problem of "knowledge" is also addressed later in the book and I will not talk much about it now (another topic for a future post!)
Now let us apply this to formal methods and the work we are all involved in as a community. What are some examples of "affordances" and "signifiers" that we can associate with? The answers are not immediately obvious, but some examples I would like to briefly discuss are:
- A function "affords" application, and a relation "affords" satisfaction
- The signifier for this is just the mathematical existence of the function/relation itself
- A finite-state automata "affords" a regular-language (and vice-versa)
- The signifier is the fact that you can follow arrows in the FSM bubble diagram and this leads to a language -- the fact that this is always a regular language is not at all obvious and is a deep result!
- A type-system "affords" programs that avoids run-time errors (sometimes!)
- The "signifier" of a type-system are the type-annotations that a programming language requires (or infers). Again the fact that this will ensure programs that do not have run-time errors is not at all obvious (or even true!)
- A program "affords" satisfaction of a specification
- Here the affordance is not so obvious: the object is a pair of program and specification. Together they beg the question of satisfaction: this is the utility/function of the object -- to demonstrate the satisfaction relation. This function itself it not at all trivial and I do not think there is any "signifier" for this. Maybe this needs to be broken up into smaller pieces.
- A proof-tree "affords" a check that it is well-formed and is a proof in a particular logic
- The signifier here is the structure of a proof-tree -- these are generally designed to indicate the inferences performed, and the rule used for each inference. The function of being checked is "afforded" by the tree-structure of the proof.
Now some of the above examples may seem a bit artificial, but I believe this is an exercise worth doing. It will focus our minds on who the users of our work are, what they are trying to achieve and how we are empowering them to achieve their goals. I believe that thinking through these concepts will help us get clarity on the value we provide as a community and help more effective communication of this to the rest of the world.
In the above examples I have avoided using tools and algorithms that are based on formal-methods -- I wanted to focus on the core artifacts that we design and use in formal methods themselves rather than the program that executes them. The affordance of a program is to "execute it", and as a community I feel we have focused on coming up with "magic" algorithms which solve difficult problems; and have struggled to explain this to the rest of the world. For the world, the main affordance of a program is to execute it -- and this does not help explain the problem that is solved!
I hope this post directs you to think a little bit about affordances and signifiers. Do you have examples in your mind that you could share? I would love to hear your ideas.
