SOL: How did you get interested in formal methods?

JW: I got interested in them when I was doing my Ph.D. thesis work. I guess I've been a flag-waver ever since. Back then, computer science was a really new field, and not much was well understood about the foundations of the field, and so I think it really goes back to my more general interest in understanding the science of computer science. And so, formal methods is really just one aspect of the science of software engineering. It was just one part of the big picture that I was interested in pursuing.

SOL: Your current interests?

JW: My current interests are in security. I think what I'm most well-known for is advocating the use of what I call “lightweight” formal methods. This gets a little technical. It's not easy to get typical software engineers to use formal methods, because they are based on mathematics, and you do need to have some minimal amount of mathematical sophistication to read formal specifications, let alone write them. The typical software engineer today is not trained to be so adept. It's unfortunate, and it really points to a societal problem with our lack of encouraging young students to study math and science. But this is a systemic problem.

So we have typical engineers who write software in industry today who are “math averse.” The way to address that is to give software engineers tools or notations and methods which give them the power of formal methods without requiring a deep, sophisticated knowledge of how the methods work. Ideally, you'd like a tool, for instance, that you could run over your code, run over something that you write, and verify certain properties of your design. And that's part of what I mean by lightweight formal methods. So you don't try to verify everything in your design, but if you verify one important thing, that's pretty good. Or you don't try to verify your whole system, you just try to verify one part of it. That's another way to do lightweight formal methods. So both techniques have really paid off in industry today, in hardware and software as well.

In particular, one of the formal methods that I think is most successful, but this is not due to me, it's due to my colleagues, is model checking. And model checking is really now a given in the hardware industry, and it's becoming more and more of interest in the software industry as well. So I think that we still have a long way to go to my dream of writing and creating more reliable software, or software that's bulletproof, or software that's completely predictable, but we do have some proven successes that point at least in the right direction.

So in any case, my current interests are in security, and that's really just what I think of as one aspect of creating systems that are more predictable and more reliable. I actually think that the broader property that you want your system to satisfy is what I would call trustworthiness, which includes reliability, security, privacy, responsibility, lots of other “-ilities.” Reliability, if you think of that as just correctness, is already a difficult enough problem. And I think security has attracted attention recently by many partly due to 9/11, of course, but also partly due to the prevalence of viruses or bugs that attackers are able to exploit in code that's widely used, like the Microsoft operating system and applications. So that's why security, and software security in particular, has become more interesting as a research topic.