As programming languages researchers, we are interested in designing beautiful abstractions, which enable sound reasoning and construction of safe sys

Programming Languages + Human-Computer Interaction: Continuing the story at SPLASH 2020

submited by
Style Pass
2021-07-06 17:00:11

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.

Leave a Comment