David Van Horn receives NSF Career Award

Assistant Professor David Van Horn has received an NSF CAREER Award for his work entitled Gradual Verification: From Scripting to Proving.  His work will investigate the theory and pragmatics of next generation programming languages that enable users to gradually adopt automated verification and formal method techniques for making software with strong behavioral guarantees.  These next generation languages will bridge the gap between today's expressive, widely-used programming languages like JavaScript and Haskell and verification-oriented languages like Coq and F*, which are used by more rarefied communities concerned with critical systems.

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.

The approach is inspired by recent work in so-called "gradually-typed" programming languages, which grew out of the PL research community, but are now undergoing major adoption efforts by Google, Facebook, Twitter, and others.  Gradually typed languages allow users to gradually migrate programs that use dynamic types, where basic sanity checks are performed at run-time to prevent ill-defined behaviors (e.g. as in JavaScript, Python, and Ruby) into more statically typed forms (e.g. as in Java, Haskell, and Scala) where these checks are formally proven ahead-of-time by the language compiler.  More static checking leads to increased confidence the code behaves as desired, reducing long-term maintenance costs and eliminating whole classes of software bugs.

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.