A major issue facing software development and maintenance is the sheer complexity of programs. Even software designs that start off simple often evolve into programs that are both brittle and hard to understand.
In this talk, I advocate programming in stages, where the programming language allows the program design to be described at varying levels of abstraction. Higher levels of abstraction focus on the intent of the design, whereas lower levels of abstraction introduce optimizations and other details. Since the layering is expressed in the programming language, the stages are preserved as part of the program text. Therefore, the stages help break down the program’s complexity not only during development but also during maintenance.
I will describe some language features, both old and new, that encourage staged development. To help communicate the vision, I will demonstrate Dafny, a research programming system whose language blends specifications, imperative programming, and staged program refinements and whose development environment is powered by an automatic program verifier that constantly analyzes the program to help the programmer get details right.
Joint work with Jason Koenig.
K. Rustan M. Leino is Senior Principal Engineer in the Automated Reasoning Group at Amazon Web Services. He works on ways to make sure programs behave as intended, secure and functionally correct. Leino is known for his work on programming methods and program verification tools and is a world leader in building automated program verification tools. These include the languages and tools Dafny, Chalice, Jennisys, Spec#, Boogie, Houdini, ESC/Java, and ESC/Modula-3. He is an ACM Fellow.
Before Amazon, Leino has been Principal Researcher at Microsoft Research, Visiting Professor at Imperial College London, and researcher at DEC/Compaq SRC. He received his PhD from Caltech (1995), before which he designed and wrote object-oriented software as a technical lead in the Windows NT group at Microsoft.
Leino hosts the Verification Corner channel on youtube. He is a multi-instrumentalist, he instructed group cardio and strength classes for many years, and he likes to cook.
