Class 2: Ethics of Proof Automation

For the second class, we will read the ACM Ethics Code.

This is a code by which all computer scientists who submit to ACM conferences are bound. It does not give you easy answers, but it does give you a useful framework to think about the ethics of your research.

It might seem kind of weird to read the ACM Ethics Code in a proof automation class. But I think ethics are as fundamental to this work as type theory is. What is any technology if we don't consider its impacts on humanity?

I never really learned this stuff in graduate school, and I really wish I had. It was Timnit Gebru and Meg Mitchell's dismissals and their fallout that really got me thinking about the ethics of my own research. And now that I'm paying attention, I realize the ethical questions are everywhere. So I hope reading this and thinking about how it interacts with proof automation will be a useful exercise for all of you.

You can find the video for the second class here, and the corresponding slides and transcript here. You can find a reading guide and the discussion questions below. The video will be posted when it is ready.

Please note that because of POPL, this reading is not due until January 25th at 10:00 AM. From next week forward, readings will be due the morning before the corresponding class.

Everyone is different here, but the way I got the most out of reading this code was by looking at each point, and thinking about how it applied to a situation that I had been in or heard about. After spending enough time doing this, I found that naturally when I encountered new situations in the wild, I'd think about particular points of the code that corresponded to it. I've found this useful not just for making decisions myself, but also for raising concerns to people in positions of power.

If you cannot think of case studies relevant to your own research or situations you have read about elsewhere, the discussion questions below may help, and you may wish to read them before reading the code in order to frame your reading.

Most of the code is, I think, about what one would expect. But there are some things I found genuinely surprising. I always disliked norms of confidentiality, but 1.7 convinced me to take it more seriously as a professional obligation. My personal favorite, though, is 2.3, which actually encourages you to challenge and in some cases break unjust rules. It's really refreshing to see that in a professional code. I also like 2.9, which makes a case for verification, and 3.6, which makes a case for automatic repair.

But not all verification work is inherently good, even though we often like to imagine that it is. Like what if your proof automation is being used to verify a drone used by the US military? This can be a major strain with 3.1, and yet this is where a lot of verification funding comes from!

Please write a short paragraph as a comment in the class forum thread about any one of the following discussion questions (you need to respond to just one question of your choice to get credit, though you're free to write more if interested):

1. Imagine that you are a professor in charge of a research group, working on proof automation that makes it easier to prove operating systems secure. DARPA offers you $10,000,000 in support of your research, with the caveat that you must demonstrate the success of your automation to build a verified operating system that makes a drone resilient to remote hijacking. Do you take the money? What ethical concerns factor into your decision? What points from the ACM Ethics Code do you find relevant?
2. When it comes to designing, building, and evaluating proof automation, it can sometimes be useful to collect proof development data. Imagine that you are a researcher building a large dataset or benchmark suite made up of real proof developments. The dataset or benchmark suite is a mix of static proof artifacts, proof developments on Github, and live proof development data. What ethical considerations do you consider in going about this data collection? What points from the ACM Ethics Code do you find relevant?
3. You are a researcher at a large tech company, working on tools that make it easier to prove code secure. You realize in the course of your work that code already deployed in production systems at the tech company has a serious security bug that puts customers at risk of harm. You raise concerns to the relevant team, and then to your manager, but after months, nothing changes. You write about it in your paper draft, but your manager orders you not to publish it, saying that it leaks confidential information. What do you try next, and why? What ethical considerations are at play here? What points from the ACM Ethics Code do you find relevant?
4. Write a paragraph responding to someone else's comment in the discussion forum.
5. Write a paragraph about any other single interesting thought, question, or idea that you had in response to the reading.

The first question is heavily inspired by a real DARPA program, though modified significantly. Both the first and second questions are inspired by experiences I've had so far during my research career.

Since the first week is asynchronous, we will not have this discussion in person. So, feel free to keep responding to each other if you find the conversation interesting---but no pressure. You'll get credit as long as you write about just one of the above.