How can types and formal reasoning tools improve the lives of people who write software? This is the focus of the HATRA (Human Aspects of Types and Reasoning Assistants) workshop. At the 2020 meeting, we discussed exciting opportunities for these key PL techniques to make developers more effective.
When developing massively distributed, interactive applications, programmers must select mechanisms that balance consistency, performance, and availability, which can be challenging. New research is looking at ways to automate this selection, with provable guarantees.
People of PL is a series of interviews with PL researchers. In today’s post, John Wickerson chats with Alexandra Silva, who is a Professor in the Department of Computer Science at UCL.
Ideas from PL research, such as functional combinators, behavioural types, and compiler correctness proofs, can be applied to distributed systems, facilitating their understanding, implementation, and formal verification.
