Semantic Foundations for Live Programming Environments

When programming, it is common to spend minutes, hours, or even days at a time working with program text where there are missing pieces, type errors, or merge conflicts. Programming environments have trouble generating meaningful feedback in these situations because programming languages typically assign formal meaning only to fully-formed, well-typed programs. Lacking timely and meaningful feedback, programmers–particularly novice programmers–struggle to maintain an accurate mental model of the behavior of the code that they are reading and writing, resulting in confusion and costly mistakes.

In this talk, I will introduce Hazel, a live functional programming environment that addresses the problem of working with incomplete programs from type-theoretic first principles. Hazel can synthesize incomplete types for incomplete programs, run incomplete programs to produce incomplete results, and perform various semantic transformations on incomplete programs. These transformations are exposed to the programmer as keyboard-driven semantic edit actions. We have formally specified each of these mechanisms using the Agda proof assistant, resulting in the first end-to-end specification for a live programming environment.

This rich semantic framework lays the foundation for a new generation of intelligent programming environments that automate away boilerplate software development tasks, leaving users to focus only on those tasks that truly require human creativity.
Cyrus Omar leads the Hazel project as a postdoc at The University of Chicago. He received his PhD from Carnegie Mellon University in May 2017. Cyrus started his research career as a neurobiologist before deciding to focus on augmenting human cognition with better programming tools.