Types, Brains and Quadcopters: Modern Programming Languages Research

This talk highlights recent results covering both traditional and
interdisciplinary programming languages research. First, we consider a
common stumbling block for new programmers: confusing type error messages.
We present an approach that synthesizes dynamic witnesses for static type
errors based on Lambda-H, our extension of the lambda calculus with
"holes" . In a blind study involving over 4,000 programs and over 100
students we find that our technique can apply to 80% of student concerns
and is more helpful than standard error messages. Second, we present results from
a novel study of how the human brain processes programming languages and
natural languages via functional magnetic resonance imaging. Informally, we
can "read minds" with 80% accuracy (p < 0.001), determining whether a subject is engaged in a prose or programming language task. We find that certain brain regions distinguish between code and prose (p < 0.001), and, critically, that this distinction is modulated by expertise ("more experienced programmers treat code more like prose at the brain level" ). Finally, we briefly present "technology transfer" -style results on the application of our automated program repair techniques to commodity quadcopters, including a video demonstration.
Westley Weimer's primary research interest is advancing software quality
through both static and dynamic programming language approaches. He is
particularly concerned with automatic or minimally-guided techniques that
can scale and be applied easily to large, existing programs. He also works
to help programmers address defects, understand programs, and program
correctly. His research spans automated program repair, formal
verification, program improvement, human studies, and language feature
design. He received his PhD from Berkeley and now serves as an associate
professor at the University of Virginia. His work has led to over 8,400
citations, eight distinguished paper awards, four multi-conference research
awards, and one ten-year most influential paper award. He also enjoys
fencing and overacting.