Why I Do the Research I Do

Main Motivations

I have always been interested in the connections between writing programs and human reasoning. How do we manage to make the mappings amongst the abstract notations of programming languages, the way those notations get interpreted by computers, and what we want to achieve with programs?

I feel that formal logic is a key element in understanding the process of programming. Formal logic was developed originally in order to model some of the reasoning capabilities of the human mind. It doesn't model how we go about finding solutions, but it does model how we express such solutions in a precise way to other people (or other things, like machines). Hence logic is a main theme of my research.

Program Verification and Testing

Research on formal methods has in the past concentrated on formal program verification; that is, on proving in a mathematically rigorous way that a program has certain formally-stated correctness or termination properties.

Many people are committed to research in this area and many others say that this research is totally useless. I am in the middle. I am disappointed at how slowly research in this area has progressed, and I think that we have to give programmers some practical support for doing the kinds of informal verification they have always been doing -- that is, by established techniques of software testing. So I am working on formal tools for helping them do this.

However, I do not despair of us ever being able to do practical program verification. I believe that De Millo, Lipton and Perlis's and Fetzer's well-known CACM papers on these topics miss the point. I believe that if Moore's Law continues to hold (speed of processors and size of memory doubling every 18 months for the same price), research into verification continues to advance, and programming languages become more precisely defined (Java continues that trend), we will eventually be able to prove the properties we want in practical ways that will have a significant impact on the practice of programming. So I am still interested in contributing to this research.

Declarative Languages

Declarative languages come up often in my research and in the research of many programming language people. In my opinion, this is because declarative languages (e.g. Lisp, Prolog, ML) are like the "fruit flies" of programming language research.

What do I mean by this? Biologists are not necessarily interested in fruit flies for their practical impact (unless they also happen to be banana farmers). They are interested in them because they are relatively simple, low-maintenance animals, which still allow us to explore ideas in genetics and biochemistry relevant to all animals.

Similarly, programming languages people are not necessarily interested in declarative languages for their practical impact (unless they also happen to be using them for AI or similar applications). They are interested in them because they have a relatively simple syntax and easy-to-define semantics, which still allow us to explore ideas in implementation, testing and verification relevant to all programming languages.