IEEE Fellow Jeannette M. Wing is President's Professor of Computer Science and head of the Computer Science Department at Carnegie Mellon University, in Pittsburgh. Her general research interests are in the areas of specification and verification, concurrent and distributed systems, and programming languages.
Prof. Wing is a member of The National Academies' Computer Science and Telecommunications Board. She is a member also of Microsoft's Trustworthy Computing Academic Advisory Board, Intel Research Pittsburgh's Advisory Board, Dartmouth's Institute for Security Technology Studies Advisory Committee, and the Idaho National Laboratory and Homeland Security Strategic Advisory Committee. She was a member of the DARPA Information Science and Technology Board and the National Science Foundation Scientific Advisory Board. She is also a member of the Sloan Research Fellowships Program Committee.
Prof. Wing has worked at Bell Laboratories, the USC Information Sciences Institute, and Xerox Palo Alto Research Center. She spent a sabbatical at MIT in 1992 and another at Microsoft Research from 2002 to 2003. She has consulted for Digital Equipment Corp., the Carnegie Mellon Research Institute, and the Jet Propulsion Laboratory.
Spectrum Online: You work on formal methods. What are formal methods?
Jeannette Wing: A method is formal if it is based on some mathematical system. And people use formal methods to describe systems so that they can check or verify or even predict the behavior properties of the system. And without a formal method you can't really do any kind of analysis, formal analysis, on a system, let alone any kind of prediction of how your system might behave in the real world. I think the best analogy to what a formal method is to a general audience is that what we do is akin to what an architect does in writing blueprints for the design of a building. If you wanted to build a new home, you wouldn't just hire a construction company and say, ”Build me a new house.” You'd first hire an architect and say, ”Please design a house for me that we can agree on, something I'll like, and then ask the construction company to build according to the blueprint.”
So what formal methods are all about is really the process of writing more formally an architectural description of the system, much like a blueprint for a house. And the practice of software engineering is that people go straight to the construction phase, and they start implementing a system without even knowing what they're supposed to implement. That's why we have a lot of software systems today that are unpredictable and unreliable and insecure. So the point about formal methods is to, in the end, create more reliable software systems, or more reliable systems in general. I think it really shows the state of practice in software engineering: We're not nearly as mature as the architectural construction industry. And we would like to be at least that mature, because the systems that we design are much more malleable, and change, and much more complex than a house.
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.
SOL: Your interest in teaching and developing the next generation of engineers?
JW: I think there are two things to your question. One is, how do we get children at the K through 12 level interested in science and engineering? How do we get them to study math and science in high school? Whether they continue on studying science or engineering or mathematics in college or not, it's basically ensuring a minimum level of mathematical sophistication by our society. And I don't see that in the United States. I don't even see that much of an effort to encourage children to stick to math and science. And I think it is a cultural problem that we all understand, and presumably school boards are aware of the problem and do their best to address it. But a lot of it has to do with parents, peers. It takes a collective effort to really stress the importance of math and science. And I'm not talking about everyone having to become scientists, I'm just talking about everyone having a minimum level of sophistication in math and science. And when you have people dropping out of math by eighth grade, you're going to have a pretty minimal level of sophistication, in contrast to, say, India and China, where you see incredibly high levels of sophistication among all grade school and high school students in math and science.
The difference is quite noticeable. So that's the first problem. And that is something that an individual as a teacher can't solve alone. But if enough of us collectively, like IEEE Spectrum and IEEE in general, and other professional organizations that support science and engineering and mathematics, get the word out and speak up about the importance of studying math and science at the grade school and high school level, then maybe we could change the culture. I don't know, maybe not in our lifetimes. But that's one of the problems, and maybe our society will never solve that problem. Certainly not when intelligent design is being taught now in high schools.
So the second problem is something a bit more specific to your question, which is my own education in education and teaching. I think that's probably just a given for any academic. I've always loved to teach. In fact, I probably knew I wanted to be a teacher before anything else. I didn't even know what I was going to teach, I just knew that I liked to teach. So of course I have an interest in teaching. As far as education goes, more broadly, I'm always thinking about two things. One is keeping curricula fresh and up-to-date and relevant, and the other is ensuring that people get their fundamentals, their foundations, because again, if you have strong foundations then you can almost do or learn anything. And there's always a balance in any kind of educational program between fundamentals and applications, if you will, or practical, state-of-the-art. You really do need to keep a balance.
I would just emphasize that right now I have a grand vision for the world. And that is perhaps partly biased, because I'm coming from computer science. But my grand vision for the world is to have everyone be able to think computationally. Let me back up. My vision is that computational thinking will be a fundamental skill used by everyone in the world by the middle of the 21st century. And if there's one thing you want to put in crazy bold letters attached to this Q&Amp;A, it's that particular vision. And the boldness of the vision is that, imagine every child, in addition to reading, writing, and arithmetic, knowing and using computational thinking. And we already have seen evidence of computational thinking influencing other sciences and engineering. It's revolutionized statistics, through machine learning, which is computational thinking. I think our interest by society today in computational biology is really an ambition from the computer science side of things to say that computational thinking can inform biology. And I think we're going to see this in nanocomputing and even quantum computing, when you want to think about computational thinking influencing physicists.
But the boldness of the vision is not that computational thinking influences just scientists, but it's everyone, So that, not perhaps in my generation but maybe in our children's generation, we will start seeing the prevalence of teaching at the grade school or high school level of ways to think like a computer scientist. And I really do think of this as a way of thinking, and a way of solving problems, and a way of defining systems, and a way, in fact, of understanding human behavior that's very, very different from any of the other kinds of ways of thinking that we know today or that children learn today. So that's quite a grand vision I have, but that's completely consistent with the complaint I told you before about ensuring and encouraging children to stick to studying math and science, and how if we can do that we can elevate the overall analytical skills and abilities of our population. We need to do that if we're going to retain an edge, if you will, in science and technology. That's why I plant this vision in people's heads today.
SOL: How would someone think computationally in daily life?
JW: I put a short piece on computational thinking on my Web page. I also put a set of slides that are based on my short piece. And I intend to actually write something up about this and submit it for publication. One is when a child is faced with a problem to solve. Theoretical computer science gives you immediately two questions to ask when you're faced with a problem to solve. The first question is, can you even solve it? This comes from a whole set of questions having to do with impossibility results. And when you're using computers you are bounded by some kind of resource. Usually it's memory. Let's just say it's memory, because you understand space as a resource. You might ask the question, given a finite amount of space, can I even solve this problem? You might also ask, given a finite amount of time, can I solve this problem?
Once they answer the question, yes, I can solve it, then the second question— which again theoretical computer science gives you a way to think about—is, how efficiently can I solve this problem? Can I solve it in linear time, log time; how much space do I need to use? That's just general. Let me give you a more systems-oriented way that one can say to a child, oh, you're thinking computationally. When a kid gets up in the morning he has to go to school. He has to put stuff in his backpack knowing what he has to do for the day. He might have certain classes he knows he's going to go to that day. Maybe he has to go to soccer practice in the afternoon or stuff like that. So he puts in his backpack all the things that he needs for that day. In systems, we call that pre-fetching and caching. Basically, it's saying, keep close to you what you're going to need either most often or � in both time and space again, you want to keep close to you what you know you're going to use. You shouldn't take your gymnastics outfit if you're going to go to soccer practice today, but tomorrow, when you go to gymnastics, you'll do the opposite. Kids today don't think about pre-fetching and caching, but they probably do what I just told you. And I'm not saying that we're going to go around and have kids using those terms, but we can elaborate on that example.
There are lots of examples. There are lots of ways in which abstract examples can be translated into real-world activities, whether it's the theoretical idea of having to search for a piece of paper in a stack of paper and what's the most efficient way to do that, or how to plan ahead for your daily activity and what are the thoughts that go through your head when figuring out your plan. Another typical example is avoiding race conditions. When you are trying to coordinate with a friend to, say, schedule a meeting somewhere, or you're sending e-mail to each other, if your message gets to them after the other person just sent you a message, before he's read your message, it's just not synchronized, and that's called a race condition. I think people understand that this happens to them all the time, and then there are ways to avoid race conditions. And so you can imagine a solution to that problem coming from computational thinking.
About the Author
Lauren Aaronson is a science and technology writer based in New York.