I attended the Future of Software Engineering Research Conference (FoSER) last weekend, in Santa Fe, NM. This was the first software engineering conference I’ve attended, and it was really interesting to get out into a community I did not know much of anything about. There were a number of friendly and familiar faces, since formal methods is firmly a part of software engineering (I had nice conversations with Ganesh Gopalakrishnan, Nishant Sinha, Chao Wang, Gary Leavens, just to name a few).
The conference was largely aimed at trying to help define future directions for funding in software engineering from NSF and other government agencies. The first day of the meeting was a blizzard of short (6 minutes, to the second) talks in 5 parallel tracks. The next day, each of those tracks broke into subgroups to craft slides summarizing ideas in a particular area. I worked with Gary, Chao, Steve Reiss, Garrin Kimmell and Frank Fu (the latter two both from our group at Iowa) on ideas for specification languages. It was a stimulating, not to say rip-roaring, discussion, and I found it quite interesting. We did manage to include a strong plug for language-based approaches to specification, in particular dependent types and typestate systems. So we did chip in our 2 cents.
Our subgroup talked a lot about trying to expand the kinds of properties that could be naturally specified (security properties, properties of graphics and layout, performance properties, maybe others), as well as the kinds of artifacts that could be specified. I am pretty intrigued by the idea of specification languages for things other than code, following this conversation. How about a specification language for Word or Office? What does it mean to specify a text document? What kind of properties should you be able to express, and how can you express them? For unstructured text, this might degenerate into a language based on string-matching, but maybe not; there could be some higher-level abstractions one might want to use in specifying text. Or how about a specification language for software style? Suppose I am Google (I would have to have around 23,000 more copies of my internal organs — a rather bulgy thought), and I want to try to enforce some coding standards. It would be great to be able to write up a high-level declarative specification of my coding rules, and have them checked automatically by a tool. Notice, the point is not to check a fixed existing set of coding rules, but rather to allow an organization to specify their own, in some high-level language. I think that sounds pretty interesting, and I could not find anything on the web to suggest that this has already been done.
Just a few notes I took down that conveyed new (to me!) ideas:
- “Software evolution is the norm” so we should think about software as an artifact over time. Refactoring and other software maintenance and transformation methods are thus more important than they’ve been given credit for. These were ideas of Ralph Johnson (U. Illinois).
- Eunsuk Kang, a doctoral student of Daniel Jackson’s at MIT, talked about design for dependability. How do we design systems to minimize the size and/or complexity of the parts of the system which are critical for our highest-priority properties? I thought this was quite a compelling idea.
- Matt Dwyer (U. Nebraska) talked about a very compelling vision for static analysis environments of the future, where a complete (or more complete) analysis of a system is achieved by combining partial results from a variety of tools. The central idea is that tools should be able to provide “partial evidence”, to export what they have learned (as opposed to what they can’t be sure about) from analyzing a piece of the system.
- Shuvendu Lahiri (MSR) commented to me that stronger static typing will become compelling to developers when it allows the compiler to remove run-time checks. In projects here at Iowa, we have definitely found that dependently typed programming can fruitfully be viewed as just a process of showing the compiler that certain run-time checks (potentially very expensive ones) are not needed.
Anyhow, so that was a little glimpse into FoSER. I left the meeting thinking that it could be interesting to try to apply some of our PL and CL (Computational Logic) techniques to software-engineering problems.
To close this post, here is a photo, courtesy of Jeff Huang (HKUST) of myself and my former undergraduate-research student Todd Schiller, currently a doctoral student at U. Washington. The PL group there is definitely doing something right, because I was really struck by how knowledgeable Todd has become about domain-specific languages (he is interested in designing these for finance applications).