As programming languages researchers, we are interested in designing beautiful abstractions, which enable sound reasoning and construction of safe systems. But ultimately, human beings employ those abstractions to construct systems in ways that make sense to them. HATRA (Human Aspects of Types and Reasoning Assistants), which debuted at SPLASH 2020, is a new workshop intended to build community and establish a research agenda on this topic. A group of thirty researchers and software engineers convened over two days to discuss the relationship between formal approaches and programmers that use them.

One theme we saw at HATRA is the diversity of goals that programmers have and the contexts in which they work, which illustrated the breadth of the potential of programming languages research. People working in large organizations may have different needs from people working individually. Some people write software to tell stories, as shown in Towards Solver-Aided Creativity (Chris Martens). Others design circuit boards (Richard Lin, Bjoern Hartmann). By creating domain-specific languages and interaction techniques, we can bring the benefits of types and formal methods to a variety of domains.

At HATRA 2020, we discussed four categories of implications of types on programming. First, types have the potential to influence human thought both for expert and novice programmers. Second, types have pragmatic benefits for users that extend beyond their safety benefits, which researchers often focus on. This leads to work on programmer experience, since types and reasoning assistants can shape the answers to high-level questions about software development. Finally, there is a need for improved adoption and development of empirical methods, particularly qualitative methods.

Types Influence Thought

Types provide a programming language designer leverage to affect human thought. Conversely, types may also help people translate thoughts into computer-legible intentions. However, we need much more research regarding in what ways and how. If types provide a decomposition principle, perhaps they are useful exactly when one knows how to decompose a problem. In contrast, when trying to explore how to decompose a problem, types can interfere with the process of exploring possible decompositions, since early versions of those decompositions may be ill-typed, and because types can increase viscosity. Programming with holes, which Hannah Potter presented, is a promising approach that could aid top-down programming by clarifying the types of terms that need to be written to complete the program. Can an extension to programming with holes help with exploration as well, particularly for beginners?

Python, a dynamically typed language, has become very popular in introductory programming courses. If static types are helpful for programming, are they not also helpful for beginners? One hypothesis is that introducing a type system requires people to learn two notional machines (the type checker as well as the operational semantics) rather than just one, making learning the language harder. Is this right? How can we design type systems that we can show benefit beginners as well as experts? Or, alternatively, of the many different programmers doing different things, which might be better off starting with a strongly typed language?

Pragmatic Benefits of Types

Types document the boundary of a module (its interface), but in many cases, not the core ideas that the module encapsulates. The completeness of that specification depends on the richness provided by the type system. In the limit, a very rich type system might expose implementation details, which arguably should not be part of the interface. How can we develop type systems that expose key aspects of module semantics without exposing their implementations?

Strong type systems have had a reputation for producing poor error messages. However, the Rust community has found that persistent work on error messages has resulted in a much more useful compiler, which helps programmers understand their mistakes and how to fix them. This observation is particularly compelling in the systems programming context of Rust, where people have typically rejected strong type systems in favor of a low level of abstraction.

Types are fundamental to programmer experience because they enable useful editor features, such as autocompletion and rename refactoring. For example, one benefit of TypeScript over JavaScript is that the types allow superior autocomplete. Similarly, the Hazel project’s adoption of syntax trees with typed holes facilitates integration with programming by voice, an important accessibility feature for programmers with limited hand mobility. As research on type systems achieves ever-stronger safety properties, we need a parallel investigation into how to use these (and more conventional) type structures to enable richer and more convenient programmer experiences. We need more research on programming language design that considers the impact on the broader experience of the programmer, including implications for IDEs, build tools, interoperability with other systems, and accessibility.

Programmer Experience

One participant observed, “I feel like we’ve barely scratched the surface of interaction modes [such as REPLs, IDEs, and code notebooks] between humans and programming language tools.” We have a variety of different approaches, but don’t know which are best in which situations and how to combine them to help programmers. Some languages separate compilation and execution, and others don’t. Some languages have REPLs. Some allow direct manipulation or use GUIs to specify some aspects of the program. Some IDEs integrate workflow features, such as bug trackers or version control systems. High-level language design decisions can facilitate or impede adoption of these techniques.

Several of the papers presented at HATRA ’20 focused on aspects of programmer experience. Will Crichton presented a paper on how ownership affects programmer experience in Rust. Dominic Orchard showed how to help programmers use units of measure in programming languages. Gongmin (Gabriel) Luo talked about visualizing ownership and borrowing in Rust.

Programmer experience is a key aspect of formal reasoning systems. April Gonçalves discussed approaches for user-friendliness in proof assistants. By using an algebraic effects system, a user can selectively leverage different proof strategies (solver, proof search, tactics) within one programming language. Alastair Reid et al. argued for meeting developers where they are to improve adoption of formal methods. One approach they proposed is to use formal verification in places where programmers might already have tests, since tests are already an expected part of development. A focus on programmer experience may be crucial to the adoption of safer programming techniques, as Jean Yang argued in an earlier post on this blog.

Empirical Methods

In what situations and for which users are types and formal reasoning tools beneficial? Conversely, in what cases might they be harmful? What forms of evidence will communities of practice find convincing? We might show people what mistakes they previously made frequently that they won’t make with the new type system. For example, how often do memory safety bugs arise in practice? Conversely, how can we use empirical methods to show where weaker requirements (perhaps paired with automation) might be beneficial? For example, web browsers support rendering invalid HTML, which makes it much easier for novices to create web pages that render.

We discussed empirical methods and observed that most of the existing empirical papers are limited to type systems that are relatively conventional, e.g. Java, C, and C++. This leaves an opportunity for empirical work with richer type systems and verification systems, along the lines of Ringer and Coblenz. One possible route could be to automatically generate and run studies regarding a language design space, allowing exploration of a much larger space than could be explored with manually-designed studies.

We discussed the need for a wider range of methods in user-centered programming language design. What should participatory design look like, given that programming language design requires significant expertise? Randomized controlled trials (RCTs) generally suffer from low external validity (the results may not generalize beyond the study’s tasks and participant population). It is also difficult to use the results of RCTs to improve designs. How can we look beyond quantitative methods, such as randomized controlled trials, and build more acceptance of qualitative methods in our communities? Finally, how can we measure emergent properties such as simplicity or ease of understanding for advanced topics, such as relaxed memory models?

Conclusion

Types and reasoning assistants promise to empower people in creating software artifacts. HATRA 2020 provided a fantastic opportunity for the community to come together to talk about how to design and evaluate techniques to help people be more effective at creating safe software. We look forward to the discussion next year at HATRA 2021!

Bio: Michael Coblenz is a Basili Postdoctoral Fellow at the University of Maryland (College Park). His research focuses on designing programming languages, such as the Obsidian smart contract language, that make programmers and software engineers more effective. Chris Martens is an Assistant Professor at North Carolina State who focuses on connections between logic and computational media. Luke Church is a Lecturer at Cambridge University who studies how to improve the experience people have when dealing with complex systems.

Disclaimer: These posts are written by individual contributors to share their thoughts on the SIGPLAN blog for the benefit of the community. Any views or opinions represented in this blog are personal, belong solely to the blog author and do not represent those of ACM SIGPLAN or its parent organization, ACM.