Abstraction as the Key to Programming, with Issues for Software Verification in Functional Languages

Abstraction is our most powerful tool for understanding the universe scientifically. In computer science, the term “abstraction” is overloaded, and its referents have not been enunciated with sufficient clarity. A deep understanding of what abstraction is and the different ways it can be employed would do much to strengthen both the research and the practice of software engineering. Specifically, this work focuses on abstraction into pure mathematics as it pertains to the intellectual complexity of computer programming. A Grand Challenge for software engineering research is to develop a verifying compiler, which takes as input a computer program and a rigorous specification of its intended behavior, and which only generates an executable if the code is proven correct via automated reasoning. The hypothetical verifying compiler would radically change the face of technology by guaranteeing that code always behaves as it should. We investigate the ways in which good abstractions, maximally exploited, can make this dream a reality. This document presents, at varying levels of technical detail, evidence for the utility of abstractions in software. We show how standard approaches to programming, even in the realm of “formal methods,” lack full abstraction. We argue that data abstraction should be achieved via purely mathematical modeling, and that this approach enables modular, scalable verification of complete system behavior. We also warn that a programming language’s formal semantics can dramatically impact the feasibility of a verifying compiler for that language. One of our main results is that the class of “functional” programming languages cannot be soundly verified by the pervasive existing methods due to an insidious and subtle issue related to data abstraction and relational specifications. We build on this unsoundness proof by sketching a new solution, and fragments of a new functional programming language that incorporates it. Advisors/Committee Members: Weide, Dr. Bruce W.