David Van Horn receives NSF Career Award
With this CAREER grant, Van Horn will promote strong practices in software development as he aims to introduce theories, tools, and a teaching framework to bring the everyday language and practice of programmers closer together with that of researchers in order to have programmers produce the most stable work possible.
Gradual types, now widely used in industry, unfortunately cannot validate all properties of a program—particularly they fall short of being able to prove partial or total correctness.
In the meantime, researchers have developed newer programming languages that can validate programs much more effectively than previous methods. However, industry has not adopted these new languages and methods as quickly as they did in the past. These newer programming languages have verification features integrated into them, but as they are not being used, industry programmers are not benefiting from the advances made by programming langague researchers. As a result, the quality and reliability of industry programmers’ work suffers, which in turn can adversely affect everyday users of their software.
Van Horn’s research seeks to bridge this gap between industry and research programs in a very practical way—by ensuring that new programmers engage in verified programming whether they are using scripting languages (such as Python) or theorem proving languages (such as Prolog or Lean). He will ensure that a new generation of programmers learn and implement verification techniques in their work from the very beginning. By teaching beginning programming using Racket, and a “systematic design process,” students are able to learn how to design a function in an intuitive manner while also learning the preliminary nation of gradual verification. Therefore, instead of postponing the teaching of programming verification until the upper level (if at all), Van Horn proposes that students learn to “reason about their programs from the moment that they are introduced to programming,” which makes for better programmers and ultimately stronger and better programs. The sooner that students learn that verification should be a part of their process of programming, the more reliable their everyday programming can be whether they end up as researchers or in industry.
Van Horn joined the Department of Computer Science as an assistant professor in 2014 and He holds a joint appointment with the University of Maryland Institute for Advanced Computer Studies. His research focuses upon the construction of reusable, trusted software components. His research includes program analysis; semantics; verification and model-checking; security; logic; complexity; and algorithms. He directs the laboratory for Programming Languages at the University of Maryland (PLUM Lab) with Professor Michael Hicks. He is the coauthor of Realm of Racket with Matthias Felleisen and undergraduates from Northeastern University, and he will be teaching a new course this summer Terps Young Scholar program in Summer 2019: Make Your Own Video Games: An Introduction to Programming and Computing.
CAREER: The Faculty Early Career Development (CAREER) Program is a Foundation-wide activity that offers the National Science Foundation's most prestigious awards in support of early-career faculty who have the potential to serve as academic role models in research and education and to lead advances in the mission of their department or organization. Activities pursued by early-career faculty should build a firm foundation for a lifetime of leadership in integrating education and research.
The Department welcomes comments, suggestions and corrections. Send email to editor [at] cs [dot] umd [dot] edu.