Abstract:
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 language definitions 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 foundations 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.
Bio:
Cyrus Omar leads the Hazel project (hazel.org) as a postdoc at The University of Chicago. He received his PhD in Computer Science in May 2017 from Carnegie Mellon University. Cyrus started his research career as a neurobiologist before deciding that we need tools that better augment human cognition if we are to truly understand human cognition.