More Sharp Languages: F#
I was perusing The Blogosphere™ today and ran across
this page about the new F# language, via
a Jason Matusow post about MS Research. It seems to be a newish functionalish language based on
ML. I just hired a programmer fresh out of CS school last autumn, and he tells me that he learned all about functional languages in school. I just kind of smiled and nodded and hired him anyway. After all, he didn't say the word "Java" during his interview.
Well, I thought I'd burn 5 minutes of my Sunday morning reading about F#, so I downloaded their introductory presentation. It turns out that F# is in use at Microsoft, integrates with VS2k3 (and 2k5), and *was used to write Static Driver Verifier*. I haven't covered SDV yet, but suffice it to say that it's kind of a static code analysis tool that verifies that you've operated the APIs correctly before you actually run the driver. It's a neat tool, and I'll be making more use of it in the future.
Microsoft has obviously turned up the heat to an unprecedented level as it relates to testing, and they've made tons of great tools available for that purpose. Other initiatives like the kernel-mode and user-mode driver frameworks are clear attempts to improve code reliability, both by creating sandboxes (usermode) and using proven code (both). The cancel-safe queue library is another example of this; safe strings are a third.
The thing that interests me is that SDV, a new testing tool (and presumably an important effort within Microsoft) was written in a functional language. The functional language people will tell you that a big advantage to that style of programming is that your programs don't have (as much) state. You'll have to look at some sample code to get an idea of what I mean, but in general, once you define a variable, there's no changing it. The lack of state makes programs easier to prove correct mathematically. In other words, using functional languages well ostensibly leads to programs that have fewer bugs, increased testability, and most importantly, provability.
I'm usually skeptical about "major advances" in programming. I am equally capable of writing excellent bugs in asm, c, and c++. Then again, proving a program correct is one of the more difficult exercises in computer science, so it just doesn't get done. Anything that can help in that regard is worth a look. As I said, I know very little about functional programming, so please don't cite any of this as authoritative. But it is interesting.
In totally unrelated news, there was no Ask Adrian session at this DevCon. That was one of the best parts of last year, so when I found out he wasn't going to be back, I asked a Microsoft person why. She something to the effect of "ooh, um, well, nobody can ask Adrian what he's working on right now!" Adrian, one of the lead devs on the kernel team, had said something about having a lot to do with Driver Verifier last time. The mind wanders. :-)
Now Playing: One by U2.