I think I've decided to take a break from my graduate course work at Auburn. I had a terrible time with the class I took last Fall (Formal Methods for Software Engineering) and this has discouraged me from continuing with school.
Not that I needed a big push, on the one hand: it's hard to work a regular job and have the discipline to come home and watch classes during the week, do regular homework and class projects, take exams, etc. And it can seem difficult to try to push yourself to learn seemingly abstract concepts that might not be directly applicable to the current technology you're using at work. [more]
However, hopefully I'm not being lazy and whiney. The formal methods class I took was about logically proving programs to be correct. In it, we learned a specification language called "Z" and tried to prove, using logical axiomatic systems, trivial programs that took many hours of thought and many pages of notes to prove. This is an interesting concept, but currently it seems not to be held as a very useful thing in software engineering practice. There are only a handful of mostly specialized examples of applications that I came across while taking the class, and I didn't really find any modern tools that use this in practice. Given this probably biased description of the class, it's probably easy to see the friction I felt while doing my course work at night, and trying to solve "real world" software engineering problems in the day at work.
Coincidentally, I saw several blog entries pop up in my feed reader towards the end of last year that seemed to express this same sentiment. Famed blogger Joel Spolsky, in a talk given to the computer science department at Yale, had this to say about the best course in computer science he ever took:
I worked on that problem for hours and hours. I had her original proof in front of me, going in one direction, which, upon closer examination, turned out to have all kinds of missing steps that were “trivial,” but not to me. I read every word about Dynamic Logic that I could find in Becton, and I struggled with the problem late into the night. I was getting absolutely nowhere, and increasingly despairing of theoretical computer science. It occurred to me that when you have a proof that goes on for pages and pages, it’s far more likely to contain errors in the proof as our own intuition about the trivial statements that it’s trying to prove, and I decided that this Dynamic Logic stuff was really not a fruitful way of proving things about actual, interesting computer programs, because you’re more likely to make a mistake in the proof than you are to make a mistake in your own intuition about what the program “f := not f” is going to do. So I dropped the course, thank God for shopping period, but not only that, I decided on the spot that graduate school in Computer Science was just not for me, which made this the single most useful course I ever took.
...trying to prove the correctness of computer programs is a lot like trying to solve a set of partial differential equations. It works great on small trivial programs, but is incredibly hard and costly on anything resembling a real world software system.
And, most recently, .Net developer Oren Eini also commented on the appropriateness of using academic knowledge in the field:
Finding a path in a graph? Design a compiler? Analyzing an image? Choosing a search algorithm? Selecting appropriate data structure for a task?
For each of those I would head for the academia, directly. Those are technical issues, and I want the academic proofs and experience there. I want the mathematical foundation for the solution.
Designing a maintainable system? Building a usable framework? Creating the domain model?
For those I am going to not going to go to the academia. I am going to go to the real world practitioner. They guys (and gals) that have been burned in the field and learned from their mistakes.
I don't think the graduate level CS courses are totally useless, by far, and I might even get the urge to continue my degree later, but for now, I'm going to focus on learning more practical technologies and drinking gently from the fire-hose of new languages, frameworks, and tools that are constantly being churned out of the interwebtubes.