The is-ought gap is a problem in moral philosophy observing that ethical judgments (“ought”) cannot be grounded purely in truth judgments (“is”): that an ought cannot be derived from an is. This gap renders the following argument invalid: “It is true that type safe languages prevent bugs and that bugs cause harm, therefore you ought to write in type safe languages”. To validate ethical claims, we must bridge the gap between is and ought with some ethical axiom, such as “I believe one ought not cause harm”.

But what do ethics have to do with manipulating programs? A lot! Ethics are central to correctness! For example, suppose an algorithm infers the type of is Bool, and is in fact a Bool; the program type checks. Is the program correct-does it behave as it ought? We cannot answer this without some ethical axioms: what does the programmer believe ought to be?

I believe one ought to design and implement languages ethically. We must give the programmer the ability to express their ethics-their values and beliefs about a program-in addition to mere computational content, and build tools that respect the distinction between is and ought. This paper is a guide to ethical language design and implementation possibilities.

William J. Bowman is an assistant professor of computer science at the University of British Columbia in Vancouver. Broadly speaking, he is interested in making it easier for programmers to communicate their intent to machines, and preserving that intent through the stages of compilation. More specifically, his research interests include secure and verified compilation, dependently typed programming, verification, and meta-programming. His recent work examines type-preserving compilation of dependently typed programming language like Coq, a technique that can enable preserving security and correctness invariants of verified software through compilation and statically enforcing those invariants in the low-level (assembly-like) code generated by compilers.