Lambda the Ultimate

I've read this site for some time, but now I have a question I believe the people at LtU could answer. The question is what are some of the current applications of formal semantics.

I've read or skimmed through some semantics textbooks, like Winskel's, and some less well-known, but a question they rarely answer in a satisfactory manner, at least to me, is why I should try to model the semantics of a language formally in the first place. Usually, the books say in the very beginning that semantics is useful for verification and program analysis, and then say no more about it. That's the reason I tried to get hold of a copy of Semantics with Applications as soon as I discovered it (an old edition is available online). The applications mentioned in the book are proving the correctness of an implementation, program analysis, and axiomatic program verification.

I've also seen recently the papers about expressing semantics in theorem provers, like here. It's cool that it is possible to extract an interpreter and a module for program analysis from the proofs about semantics. But we could just code the interpreter and program analysis; yes, I know, extracting them from a prover makes them more trustworthy. I refrain from saying that they are "correct" because it would depend on the correctness of the theorem prover, the compiler for the language, the extraction process, etc. Also, I don't know how this idea would fare in bigger, more realistic languages.

So, although I have seen already some applications of formal semantics, nothing of it quite managed to impress me much. What is it, then, that we gain by modeling the semantics of a language formally? What we can accomplish with a semantics that we couldn't without? What would be possible without a formal semantics, but difficult and/or clumsy? What examples do we have of sucessful and important applications of formal semantics to programming practice?

I think this is very much worth knowing, the questions are worth asking, and the books don't provide answers. So maybe LtU can :)

This may be slightly off-topic, but I was wondering if some of you in the community could point me in the right direction with some questions I have about a career in computer science research. To give you some background, I recently graduated from college with a CS degree, and I'm currently working for a small-to-medium-sized consulting firm doing software development in .NET.

Lately I've been thinking that software development in general might not be for me, and that I might be better off getting into research, or at least something closer to it. I feel like most of the problems I run into in my work are not that difficult, and that I just won't be putting all of my technical skills to good use in this line of work. I want to work on technical problems with some real "meat" on them, instead of just putting buttons on a form. One of my interest areas is programming languages, which is why I've come here for advice.

I guess I was initially turned off from graduate school and research after I read this article on Joel on Software, specifically the part about the dynamic logic class. After seeing that, I thought that the only way to do work that would actually make it to the "real world" would be to get into software development. I realize now that that's not entirely true, but I'm still concerned about making sure any work I do is useful, and doesn't solve a problem that no one cares about.

With all of that said, here are my questions:

• Can anyone explain to me, or link to an article that explains, the general timeline of research getting implemented in industry? I at least have a vague idea of how researchers find problems, come up with solutions, and publish papers, but from that point there's a gap in my knowledge - how does the information from that paper trickle down to a point where developers in the trenches like me know about it? I know not every piece of research is used everywhere, but something like object-oriented programming might be a good example: It originally started, more or less, with Simula and Smalltalk. How did it get to the point where practically every developer uses it, and bookstores are filled with shelves on design patterns and object-oriented languages like Java and C#?
• As a follow-up to my first question, are there careers that bridge that gap between research and industry (in this case, specifically in programming languages)? Is there a job where one can read research that others have done, evaluate it, and decide if it would be useful to put that work into some form usable by the masses? And if so, what kind of path would one take to get there? Grad school? Climb the ladder at a certain kind of company?
• Am I at all justified in being concerned about the usefulness of my work if I were to go into research? Is that something that researchers worry about, or does it tend to not be an issue?

As you can possibly tell, I'm primarily just ignorant of the various options out there, and trying to figure out what they are. As a result, any answers, advice, or links to relevant information are appreciated, and thank you for reading this long message.